perm filename PROVE2.NEW[1,JRA]2 blob
sn#017890 filedate 1972-12-27 generic text, type T, neo UTF8
(DEFPROP NEWPROOF
(NIL NEWPROOF
ALLPOS
RESTRAT
RESTRAT1
RESTRAT2
RESTRATS
ALLNEG
ANCESTOR
APPLYTEMP
APPTEMP
BARF
SEARCH1
CONST
HERE
VAR
ISCLS
ISCL
ISLIT
ISTRM
MKWRD
NEG
NEGBIT
POS
POSBIT
SEARCH
NUM
NEGL
ANCESTRY
APPENDIT
ANDOR
ASSOC1
ATTEMPT
ATTEMPTUNTIL
ATTEMPT1
AUTO
BAKSUB
BOOKEEP
CHOICE
CHOICE1
CLAUSES
CLAUSES2
CLAUSES1
CNF
CNF1
CNF2
CNF3
CNVT
CNVT2
CNVT3
COPY
COPYDELETED
DEMOD
DEM
DEPTH
DEPTH1
DEL
DOML
DOMC
DOWN
EDIT
ERPRINT
ERPRIN1
EXPUNGE
FINI
FIRSTS
FIXNEG
FIXQFF
FIXQFF1
GENSKOLEM
GETNAME
GETVARS
GOLIST
GOLIST1
INCLAUSES
INITIAL
INITIALAX
INITIALAX1
MAPIT
MATCHER
MATCH1
MATCHTR
MATCHPN
MATMLT
MATMLT*
MAX
MEMC
MIN1
MINIMIZE
MIN
MKSYM
MODEL
NCONC1
NEGATE
NEGSGN
NOSYM
OCR
OCR1
ONEGSGN
*NOPOINT
OCCUR
ORDER
ORDEREQUAL
PARMOD
PARMOD1
POTZ
PRECNF
PROOF1
PROVE
PRPAR
PRFPRINT
PRFPR1
PROOF
PTRS
QUERY
REAL-LNGTH
REDUCER
REENTER
RESTORE
RESTORE1
RESOLVE
RESTS
RESOLVE1
RESTART
RESET
RESET1
SAVE
SAVE1
SET1
SET2
SET3
SETUP
SEARCH2
S2
SETQUERY
SETQUERY1
SETQUERY2
SUBS3TA
SUBS3T**
SUB*
SUBSKOL
SUPPORT
SUBSUME1
SUBS2T
SUBS3T
SUBSUME
SUBSUME*
SUBST1
TCOPY
TEMPLATE
TERMS
TERMS1
TERMS2
TIMEIT
TREE
TREEDEP
TRY
TRY1
TRYPRF
TRAVERSE
UNIT
UNITS
UNITRES
UNITREDUCT
UNITPN
UNIFY
UNI
UNION
UNWIND
UPDATE
UPGETL
UPGETNU
UPDATESTATE
UPIT
UPIT1
UP1A
UP1B
VARIT
VINE
<)
VALUE)
(DEFPROP ALLPOS
(LAMBDA (C) (LIST (QUOTE NULL) (LIST (QUOTE CADAR) (CADR C))))
MACRO)
(DEFPROP RESTRAT
(LAMBDA(L)
(LIST (QUOTE COND)
(LIST (LIST (QUOTE NULL) (CADR L))
(LIST (QUOTE RESTRAT1) (CADR L) (CADDR L))
(LIST (QUOTE GO) (CADDDR L)))))
MACRO)
(DEFPROP RESTRAT1
(LAMBDA(L)
(LIST (QUOTE COND)
(LIST (LIST (QUOTE EQ) (LIST (QUOTE SETQ) (CADR L) (QUOTE (READ))) (QUOTE ESCAPE))
(QUOTE (PRINT (QUOTE RESETTING-TO:)))
(LIST (QUOTE GO) (CADDR L)))))
MACRO)
(DEFPROP RESTRAT2
(LAMBDA(M)
(LIST (QUOTE COND)
(LIST (QUOTE (EQ (SETQ Z6 (READ)) (QUOTE Y))) (LIST (QUOTE RESTRAT1) (CADR M) (CADDR M)))
(LIST (QUOTE (EQ Z6 ESCAPE)) (QUOTE (PRINT (QUOTE RESETTING-TO))) (LIST (QUOTE GO) (CADDR M)))))
MACRO)
(DEFPROP RESTRATS
(LAMBDA(L)
(LIST (QUOTE COND)
(LIST (LIST (QUOTE EQ) (LIST (QUOTE SETQ) (CADR L) (QUOTE (READ))) (QUOTE ESCAPE))
(QUOTE (PRINT (QUOTE RESETTING-TO:)))
(LIST (QUOTE GO) (CADDR L)))))
MACRO)
(DEFPROP ALLNEG
(LAMBDA (C) (LIST (QUOTE EQ) (LIST (QUOTE CADAR) (CADR C)) (LIST (QUOTE CDR) (CADR C))))
MACRO)
(DEFPROP ANCESTOR
(LAMBDA (X) (LIST (QUOTE CDDDAR) (CADR X)))
MACRO)
(DEFPROP APPLYTEMP
(LAMBDA(L)
(PROG (Z L1 S)
(SETQ S (CDR (ASSOC (CAR L) TEMPLATELIST)))
(COND
((NOT (EQ (LENGTH (CAR S)) (LENGTH (CDR L))))
(PRINT (QUOTE MISMATCH-IN-TEMPLATE-VARIABLES))
(ERR NIL)))
(SETQ L1 (CDR L))
A (SETQ Z (NCONC (APPTEMP (FIRSTS L1) S) Z))
(SETQ L1 (RESTS L1))
(COND ((NULL L1) (RETURN Z)))
(GO A)))
FEXPR)
(DEFPROP APPTEMP
(LAMBDA(L TEMP)
(PROG (L2 L3)
(SETQ L3 (CAR TEMP))
(SETQ L2 (CDR TEMP))
A (SETQ L2 (SUBST (CAR L) (CAR L3) L2))
(SETQ L (CDR L))
(SETQ L3 (CDR L3))
(COND (L3 (GO A)))
(RETURN L2)))
EXPR)
(DEFPROP BARF
(LAMBDA (L) (QUOTE (PRINT (QUOTE (DO YOU WANT TO CHANGE IT (Y / N))))))
MACRO)
(DEFPROP SEARCH1
(LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) NIL))
MACRO)
(DEFPROP CONST
(LAMBDA (X) (LIST (QUOTE NULL) (LIST (QUOTE CDR) (CADR X))))
MACRO)
(DEFPROP HERE
(LAMBDA (X) (LIST (QUOTE CAAR) (CADR X)))
MACRO)
(DEFPROP VAR
(LAMBDA (L) (LIST (QUOTE NUMBERP) (CADR L)))
MACRO)
(DEFPROP ISCLS
(LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 1))
MACRO)
(DEFPROP ISCL
(LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 2))
MACRO)
(DEFPROP ISLIT
(LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 3))
MACRO)
(DEFPROP ISTRM
(LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 4))
MACRO)
(DEFPROP MKWRD
(LAMBDA (L) (LIST (QUOTE CDDAR) (CADR L)))
MACRO)
(DEFPROP NEG
(LAMBDA (X) (LIST (QUOTE EQ) (QUOTE ESCAPE) (LIST (QUOTE CAR) (CADR X))))
MACRO)
(DEFPROP NEGBIT
(LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X)))
MACRO)
(DEFPROP POS
(LAMBDA (X) (LIST (QUOTE NOT) (LIST (QUOTE NEG) (CADR X))))
MACRO)
(DEFPROP POSBIT
(LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X)))
MACRO)
(DEFPROP SEARCH
(LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) (CADR X)))
MACRO)
(DEFPROP NUM
(LAMBDA (C) (LIST (QUOTE CAAAR) (CADR C)))
MACRO)
(DEFPROP NEGL
(LAMBDA (C) (LIST (QUOTE CADAR) (CADR C)))
MACRO)
(DEFPROP ANCESTRY
(LAMBDA(LLST)
(PROG (Z1 Z2 R M)
(SETQ CNT (ADD1 (LENGTH CLAUSES)))
TRY3 (COND ((NOT (HERE (CAR EE))) (GO TRY7)))
(SETQ M (CHOICE1 (CAR EE) LLST))
(COND ((NULL M) (GO TRY7)))
(SETQ Z1 (CAR EE))
TRY2 (SETQ Z2 (CAR M))
(COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
TRY1 (COND ((NOT STRATEGY) (GO TRY1A)))
(COND ((STRATEGY Z1 Z2) (GO TRY1A)) (T (GO TRY6FA)))
TRY1A
(COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)) ((AND (ALLNEG Z1) (ALLNEG Z2)) (GO TRY8)))
(SETQ R (RESOLVE Z1 Z2))
(COND ((NULL R) (GO TRY6A)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
TRY6A
TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6FA)))
(SETQ R (PARMOD Z1 Z2))
(COND ((NULL R) (GO TRY6FA)))
(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
TRY6FA
TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
(SETQ M (CDR M))
(COND (M (GO TRY2)))
TRY7 (SETQ EE (CDR EE))
(COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
TRY12
(PRINT (QUOTE COUNT))
(PRINT COUNT)
(PRINT (QUOTE LEVEL))
(PRINT LVL)
(SETQ LVL (ADD1 LVL))
(PRINT (QUOTE ELAPSED-TIME))
(PRINT (TIMEIT))
(COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
(PRINT (QUOTE NO-PROOF-FOUND))
(COND (AUTO (ERR (QUOTE NOPROOF))))
(UPDATE CLAUSES)
(COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
(ERR (QUOTE NOPROOF))))
EXPR)
(DEFPROP ANCESTRY
(NIL . T)
VALUE)
(DEFPROP APPENDIT
(LAMBDA(X Y)
(PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
EXPR)
(DEFPROP ANDOR
(LAMBDA(C UNL EXL PF)
(PROG (Z1 Z2)
(SETQ Z1 (CADR C))
(SETQ Z2 (CADDR C))
(COND
((OR (AND (EQ (CAR C) (QUOTE AND)) PF) (AND (EQ (CAR C) (QUOTE OR)) (NOT PF)))
(RETURN (LIST (QUOTE AND) Z1 Z2)))
((EQ (CAR Z1) (QUOTE AND))
(RETURN
(LIST (QUOTE AND)
(CNF1 (LIST (QUOTE OR) (CADR Z1) Z2) UNL EXL T)
(CNF1 (LIST (QUOTE OR) (CADDR Z1) Z2) UNL EXL T))))
((EQ (CAR Z2) (QUOTE AND))
(RETURN
(LIST (QUOTE AND)
(CNF1 (LIST (QUOTE OR) (CADR Z2) Z1) UNL EXL T)
(CNF1 (LIST (QUOTE OR) (CADDR Z2) Z1) UNL EXL T))))
(T (RETURN (LIST (QUOTE OR) Z1 Z2))))))
EXPR)
(DEFPROP ASSOC1
(LAMBDA (X L) (COND ((NULL L) NIL) ((EQ (CDR X) (CDAAR L)) (CAR L)) (T (ASSOC1 X (CDR L)))))
EXPR)
(DEFPROP ATTEMPT
(LAMBDA(Z S C)
(PROG (NEWNAME SUPPORT
EDITSTRAT
LCL
LVL
CNT
XYZ2
LSTCLS
LLST
Z1
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
STRATEGY
STRAT
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST
XYZ
XYZ1
COND
UNAXP
UNAXN
SAT
EE
EE1
XX
CLAUSES
SUBCLAUSES
COUNT)
(SETQ TBL (SET1 (APPEND PREFN INFN)))
(SET3 Z)
(SETQ Z (MINIMIZE Z))
(SETQ NEWNAME (INITIAL Z))
(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
(SETQ COND C)
(SETQ XYZ2 Z)
(SETQ LVL 1)
(SETQ COUNT 0)
(SETQ Z (UNITPN XYZ2))
(SETQ UNAXP (CAR Z))
(SETQ UNAXN (CDR Z))
(SETQ CLAUSES XYZ2)
(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
(SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
(T (SETQ SUBCLAUSES CLAUSES)))
(SETQ LCL (LAST CLAUSES))
(SETQ LSTCLS LCL)
(COND (ANCESTRY (GO AA)))
(SETQ XX (CONS CLAUSES CLAUSES))
(SETQ EE CLAUSES)
(SETQ EE1 (LAST EE))
(SETQ CNT (LENGTH XYZ2))
BB (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
(EVAL
(LIST (QUOTE OUTC)
(LIST (QUOTE OUTPUT)
(QUOTE PRF)
(QUOTE DSK:)
(CONS (READLIST
(CONS (QUOTE #)
(CONS (SETQ PRNO (ADD1 PRNO))
FILENAM)))
(QUOTE PRF)))
NIL)))
(QUERY)
(PROOF LHP RHP)
(OUTC Z T)
(RETURN Z1))
(T (RETURN Z1)))
AA (SETQ XYZ XYZ2)
(SETQ EE CLAUSES)
(SETQ EE1 (LAST CLAUSES))
CC (SETQ LLST (CONS (CAR XYZ) LLST))
(SETQ XYZ (CDR XYZ))
(COND (XYZ (GO CC)) (T (GO BB)))))
EXPR)
(DEFPROP ATTEMPTUNTIL
(LAMBDA (L S C) (ATTEMPT (INITIALAX L) S C))
EXPR)
(DEFPROP ATTEMPT1
(LAMBDA (L) (COND (ANCESTRY (ANCESTRY LLST)) (T (TRYPRF L))))
EXPR)
(DEFPROP AUTO
(LAMBDA(XX)
(PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
(COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
(SETQ PDEPTH 3)
(SETQ DDEPTH 4)
(COND
((NULL EQUAL) (PRINT (QUOTE (IS THERE AN EQUALITY PREDICATE (Y / N))))
(COND
((EQ (READ) (QUOTE Y)) (PRINT (QUOTE (WHAT IS IT)))
(SETQ PFLG NIL)
(SETQ EQUAL (READ))))))
(SETQ X1 XX)
(SETQ M (SETQ D 0))
A (SETQ M (MAX M (LENGTH (CDAR X1))))
(SETQ D (MAX D (DEPTH (CDAR X1))))
(SETQ Z2 (CAR X1))
(COND
((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
(SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
(SETQ X1 (CDR X1))
(COND ((CDR X1) (GO A)))
(SETQ Z2 (ASSOC (QUOTE THEOREM) NEWNAME))
(COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
B (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
C (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
(COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
(COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
(COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
(COND (SUPPORT (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))))
(SETQ ANCESTRY T)
(SETQ EDITSTRAT
(QUOTE (LAMBDA (C) (OR (GREATERP (LENGTH (CDR C)) LENGTH) (GREATERP (DEPTH (CDR C)) DEPTH)))))
(SETQ DEBUG T)
(COND (DLIST (SET3 DLIST)))
(RETURN
(LIST STRATEGY
SUPPORT
EDITSTRAT
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST))))
EXPR)
(DEFPROP AUTO
(NIL . T)
VALUE)
(DEFPROP BAKSUB
(LAMBDA(L R)
(PROG (Z U1 U4)
(SETQ Z L)
ED4 (COND ((NOT Z) (RETURN NIL)) ((NOT (HERE (CAR Z))) (GO ED6A)))
(SETQ U1 R)
ED3 (SETQ U4 (CAR Z))
ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
ED6 (SETQ U1 (CDR U1))
(COND (U1 (GO ED1)))
ED6A (SETQ Z (CDR Z))
(GO ED4)
ED2 (DEL U4)
(GO ED4)))
EXPR)
(DEFPROP BOOKEEP
(LAMBDA(L M N)
(PROG (U)
B1 (SETQ U M)
B3 (RPLACD (CDAAR U) (CONS 0 N))
(SETQ U (CDR U))
(COND ((NULL U) (RETURN (NCONC L M))))
(GO B3)))
EXPR)
(DEFPROP CHOICE
(LAMBDA(X E E1)
(PROG (Z1 Z2)
(SETQ Z1 (CAR X))
(SETQ Z2 (CDR X))
B (COND ((EQ Z2 E1) (GO A)) (T (RETURN (RPLACD X (CDR Z2)))))
A (SETQ Z1 (CDR Z1))
(COND ((EQ Z1 E1) (RETURN T)) (T (RETURN (PROG2 (RPLACA X Z1) (RPLACD X E)))))))
EXPR)
(DEFPROP CHOICE1
(LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
EXPR)
(DEFPROP CLAUSES
(LAMBDA (U) (PROG (DEBUG) (SETQ DEBUG T) (RETURN (CLAUSES1 U 1))))
EXPR)
(DEFPROP CLAUSES2
(LAMBDA (U) (CLAUSES1 U CNT))
EXPR)
(DEFPROP CLAUSES1
(LAMBDA(U N)
(PROG NIL
(COND ((NOT DEBUG) (RETURN NIL)))
(COND ((NULL (CAR U)) (RETURN NIL)))
CL1 (COND ((NULL U) (RETURN NIL)))
(UP1A (CAR U) N)
CL2 (SETQ U (CDR U))
(SETQ N (ADD1 N))
(GO CL1)))
EXPR)
(DEFPROP CNF
(LAMBDA(C1)
(PROG (C)
(SETQ C (PRECNF C1))
(RETURN (CNF2 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) NIL NIL NIL)) (T (CNF1 C NIL NIL T)))))))
EXPR)
(DEFPROP CNF1
(LAMBDA(C UNL EXL PF)
(COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) UNL EXL (COND (PF NIL) (T T))))
((MEMQ (CAR C) (QUOTE (AND OR)))
(ANDOR (LIST (CAR C) (CNF1 (CADR C) UNL EXL PF) (CNF1 (CADDR C) UNL EXL PF)) UNL EXL PF))
((OR (AND (EQ (CAR C) (QUOTE FA)) PF) (AND (EQ (CAR C) (QUOTE TE)) (NOT PF)))
(CNF1 (CADDR C) (APPEND (CADR C) UNL) EXL PF))
((OR (EQ (CAR C) (QUOTE FA)) (EQ (CAR C) (QUOTE TE)))
(CNF1 (CADDR C) UNL (APPEND (GENSKOLEM (CADR C) UNL) EXL) PF))
(PF (SUBSKOL C EXL))
(T (CONS ESCAPE (SUBSKOL C EXL)))))
EXPR)
(DEFPROP CNF2
(LAMBDA(C)
(COND ((EQ (CAR C) (QUOTE AND)) (APPEND (CNF2 (CADR C)) (CNF2 (CADDR C))))
((EQ (CAR C) (QUOTE OR)) (LIST (CNF3 C)))
(T (LIST (LIST C)))))
EXPR)
(DEFPROP CNF3
(LAMBDA (C) (COND ((NOT (EQ (CAR C) (QUOTE OR))) (LIST C)) (T (APPEND (CNF3 (CADR C)) (CNF3 (CADDR C))))))
EXPR)
(DEFPROP CNVT
(LAMBDA(Z)
(PROG (ZP ZN VARL VARNO)
(SETQ VARNO 0)
(COND
((EQ (LENGTH Z) 1)
(RETURN (COND ((EQ (CAAR Z) ESCAPE) (LIST (QUOTE NOT) (CNVT2 (CDAR Z)))) (T (CNVT2 (CAR Z)))))))
A1 (COND ((EQ (CAAR Z) ESCAPE) (GO AN1)))
(SETQ ZP (CNVT2 (CAR Z)))
AP1 (SETQ Z (CDR Z))
(COND ((NULL Z) (GO AN2)) ((EQ (CAAR Z) ESCAPE) (GO AN1)))
(SETQ ZP (LIST (QUOTE OR) (CNVT2 (CAR Z)) ZP))
(GO AP1)
AN1 (SETQ ZN (CNVT2 (CDAR Z)))
AN1B (SETQ Z (CDR Z))
AN1A (COND ((NULL Z) (GO AN2)))
(SETQ ZN (LIST (QUOTE AND) (CNVT2 (CDAR Z)) ZN))
(GO AN1B)
AN2 (COND ((NULL ZP) (RETURN (LIST (QUOTE NOT) ZN)))
((NULL ZN) (RETURN ZP))
(T (RETURN (LIST (QUOTE IMP) ZN ZP))))))
EXPR)
(DEFPROP CNVT2
(LAMBDA(X)
(COND ((ATOM X) X)
((VAR (CAR X)) (CONS (CNVT3 (CAR X)) (CNVT2 (CDR X))))
((CONST (CAR X)) (CONS (CAR X) (CNVT2 (CDR X))))
(T (CONS (CNVT2 (CAR X)) (CNVT2 (CDR X))))))
EXPR)
(DEFPROP CNVT3
(LAMBDA(X)
(PROG (Z)
(SETQ Z (ASSOC X VARL))
(COND (Z (RETURN (CDR Z))))
(SETQ VARL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARL))
(RETURN VARNO)))
EXPR)
(DEFPROP COPY
(LAMBDA (X) (COND ((ATOM X) X) (T (CONS (COPY (CAR X)) (COPY (CDR X))))))
EXPR)
(DEFPROP COPYDELETED
(LAMBDA (X) (LIST (CONS (CONS NIL (CDAR X)) (CDR X))))
EXPR)
(DEFPROP DEMOD
(LAMBDA(X L)
(PROG (S1 S2)
B (SETQ S1 (CDAR X))
A (COND ((NEG (CAR S1)) (DEM (TCOPY (CDR (SETQ S2 (CDAR S1)))) 1 DDEPTH L))
(T (DEM (TCOPY (CDR (SETQ S2 (CAR S1)))) 1 DDEPTH L)))
(COND ((EQ (CAR S2) EQUAL) (ORDEREQUAL (CDR S2))))
(SETQ S1 (CDR S1))
(COND (S1 (GO A)))
(RETURN X)))
EXPR)
(DEFPROP DEM
(LAMBDA (T1 M N L) (COND ((OR (NULL T1) (EQ N M)) NIL) (T (PROG2 (DEM (PTRS T1) (ADD1 M) N L) (SUB* T1 L)))))
EXPR)
(DEFPROP DEPTH
(LAMBDA(Z)
(PROG (Z1 Z2)
(SETQ Z1 0)
D1 (COND ((NEG (CAR Z)) (SETQ Z2 (CDDAR Z))) (T (SETQ Z2 (CDAR Z))))
(SETQ Z1 (MAX Z1 (DEPTH1 Z2)))
(SETQ Z (CDR Z))
(COND (Z (GO D1)))
(RETURN Z1)))
EXPR)
(DEFPROP DEPTH
(NIL . 10)
VALUE)
(DEFPROP DEPTH1
(LAMBDA(Z)
(PROG (Z1)
(SETQ Z1 0)
D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2)))
(SETQ Z1 (MAX Z1 (ADD1 (DEPTH1 (CDAR Z)))))
D2 (SETQ Z (CDR Z))
(COND (Z (GO D1)))
(RETURN Z1)))
EXPR)
(DEFPROP DEL
(LAMBDA (C) (RPLACA (CAR C) NIL))
EXPR)
(DEFPROP DOML
(LAMBDA NIL (TERMS1 (COND ((NEG (CAR L)) (CDDAR L)) (T (CDAR L))) 100))
EXPR)
(DEFPROP DOMC
(LAMBDA NIL (CDR C))
EXPR)
(DEFPROP DOWN
(LAMBDA(N L)
(PROG NIL
(COND ((NOT (AND (NUMBERP N) (GREATERP N 0))) (RETURN NIL)))
D1 (SETQ N (SUB1 N))
(COND ((ZEROP N) (RETURN L)))
(SETQ L (CDR L))
(COND (L (GO D1)))
(RETURN NIL)))
EXPR)
(DEFPROP EDIT
(LAMBDA(U Z)
(PROG (RES1 U1 U4)
ED4 (COND ((NULL Z) (RETURN RES1)))
(SETQ U4 (CAR Z))
(COND ((EDITSTRAT U4) (GO ED2)))
(SETQ U1 SUBCLAUSES)
ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
ED6 (SETQ U1 (CDR U1))
(COND (U1 (GO ED1)))
(SETQ U1 (CDR Z))
(COND ((NULL U1) (GO ED5)))
ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
ED7 (SETQ U1 (CDR U1))
(COND (U1 (GO ED3)))
ED5 (SETQ RES1 (CONS U4 RES1))
ED2 (SETQ Z (CDR Z))
(GO ED4)))
EXPR)
(DEFPROP ERPRINT
(LAMBDA (X) (COND (DEBUG (PRINT X))))
EXPR)
(DEFPROP ERPRIN1
(LAMBDA (X) (COND (DEBUG (PRIN1 X))))
EXPR)
(DEFPROP EXPUNGE
(LAMBDA (L) (PROG NIL A (COND ((NULL L) (RETURN NIL))) (DEL (CAR L)) (SETQ L (CDR L)) (GO A)))
EXPR)
(DEFPROP FINI
(LAMBDA(U R Z1 Z2 E)
(PROG (Z)
(COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
(COND ((NULL R) (RETURN 0)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
(SETQ COUNT (PLUS COUNT (LENGTH R)))
(SETQ R (EDIT U R))
(CLAUSES2 R)
(COND ((NULL R) (RETURN 0)))
(BAKSUB CLAUSES R)
(BOOKEEP E R (CONS Z1 Z2))
(SETQ Z (UNITPN R))
(SETQ UNAXP (APPEND (CAR Z) UNAXP))
(SETQ UNAXN (APPEND (CDR Z) UNAXN))
(RETURN (LENGTH R))))
EXPR)
(DEFPROP FIRSTS
(LAMBDA(L)
(PROG (Z)
F (COND ((ATOM (CAR L)) (SETQ Z (CONS (CAR L) Z))) (T (SETQ Z (CONS (CAAR L) Z))))
(SETQ L (CDR L))
(COND (L (GO F)))
(RETURN (REVERSE Z))))
EXPR)
(DEFPROP FIXNEG
(LAMBDA (X) (COND ((EQ (CAR X) ESCAPE) (LIST (QUOTE NOT) (COPY (CDR X)))) (T (COPY X))))
EXPR)
(DEFPROP FIXQFF
(LAMBDA(C)
(PROG (Z)
(SETQ Z (FIXQFF1 C NIL NIL NIL))
(COND ((NULL (CAR Z)) (RETURN C)) (T (RETURN (LIST (QUOTE FA) (CAR Z) C))))))
EXPR)
(DEFPROP FIXQFF1
(LAMBDA(C NEW FA TE)
(PROG (Z)
(COND ((NULL C) (RETURN (CONS NEW (CONS FA TE))))
((EQ (CAR C) (QUOTE FA)) (RETURN (FIXQFF1 (CADDR C) NEW (APPEND (CADR C) FA) TE)))
((EQ (CAR C) (QUOTE TE)) (RETURN (FIXQFF1 (CADDR C) NEW FA (APPEND (CADR C) TE))))
((EQ (CAR C) (QUOTE NOT)) (RETURN (FIXQFF1 (CADR C) NEW FA TE)))
((MEMQ (CAR C) (QUOTE (AND OR IMP EQUIV))) (SETQ Z (FIXQFF1 (CADR C) NEW FA TE))
(RETURN
(FIXQFF1 (CADDR C) (CAR Z) (CADR Z) (CDDR Z)))))
(SETQ Z (GETVARS (COND ((NEG C) (CDDR C)) (T (CDR C)))))
A (COND ((NULL Z) (RETURN (CONS NEW (CONS FA TE))))
((OR (MEMBER (CAR Z) NEW) (MEMBER (CAR Z) FA) (MEMBER (CAR Z) TE)) (GO B)))
(SETQ NEW (CONS (CAR Z) NEW))
B (SETQ Z (CDR Z))
(GO A)))
EXPR)
(DEFPROP GENSKOLEM
(LAMBDA(VARL UNL)
(PROG (Z)
A (COND ((NULL VARL) (RETURN Z)))
(SETQ Z (CONS (CONS (CAR VARL) (CONS (MKSYM) UNL)) Z))
(SETQ VARL (CDR VARL))
(GO A)))
EXPR)
(DEFPROP GETNAME
(LAMBDA(X L)
(PROG (Z)
(SETQ Z (ASSOC X L))
(COND (Z (RETURN (CDR Z))))
(PRINT X)
(PRINC (QUOTE IS-AN-UNBOUND-NAME))
(RETURN NIL)))
EXPR)
(DEFPROP GETVARS
(LAMBDA(C)
(PROG (Z)
A (COND ((VAR (CAR C)) (SETQ Z (CONS (CAR C) Z)))
((CONST (CAR C)) NIL)
(T (SETQ Z (APPEND (GETVARS (CDAR C)) Z))))
(SETQ C (CDR C))
(COND (C (GO A)))
(RETURN Z)))
EXPR)
(DEFPROP GOLIST
(NIL (EO . UEO1)
(DS . UDS1)
(CH . UCH1)
(SY . USY1)
(CU . UCU1)
(FL . UFL1)
(DI . UDI1)
(ST . UST1)
(HA . UST1)
(DE . UDE1)
(IN . UIN1)
(EV . UEV1)
(QU . UQU1)
(TR . UTR1)
(UP . UUP1)
(ME . UME1)
(SI . USI1)
(SE . USE1)
(DO . UDO1)
(CL . UCL1)
(SU . USU1)
(AN . UAN1)
(TE . UTE1)
(RE . URE1)
(SA . USA1)
(PA . UPA1)
(AS . UAS1)
(ED . UED1)
(US . UUS1)
(PR . UPR1)
(FU . UFL2)
(FD . UFL3)
(GO . UGO1)
(EX . UEX1)
(AB . UAB1)
(HE . UHE1))
VALUE)
(DEFPROP GOLIST1
(NIL (AS . AS1) (AT . AT1) (LE . EX1) (SA . S1) (CL . C1) (EX . EXP1) (UP . UPDAT))
VALUE)
(DEFPROP INCLAUSES
(LAMBDA NIL
(PROG (Z AXNO)
(SETQ AXNO (QUOTE AXIOM))
A (SCANSET)
(START)
(SETQ ZIN (ERRSET (<INPUT>) T))
(SCANRESET)
(COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
(SETQ ZIN (TOP))
(COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z)) ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A)))
(OUT >S< ZIN)
(SETQ Z
(APPEND Z
(SETUP
(CNF
(COND ((EQ AXNO (QUOTE THEOREM)) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
(GO A)))
EXPR)
(DEFPROP INITIAL
(LAMBDA(L)
(PROG (ST Z Z1 Z2)
A (SETQ Z (CDR (ANCESTOR (CAR L))))
(COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
(T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
(SETQ Z2 (CONS (CAR L) Z2))
(SETQ L (CDR L))
(COND (L (GO A)))
(RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
EXPR)
(DEFPROP INITIALAX
(LAMBDA(L)
(PROG (Z Z1 Z2 Z3 AXNO)
(SETQ AXNO (CAR L))
(SETQ L (CDR L))
A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
(SETQ Z1 (ANCESTOR (CAR L)))
(COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
(SETQ Z2 (ANCESTOR Z))
(RPLACA Z2 Z1)
(RPLACD Z2 AXNO)
(SETQ Z3 (CONS Z Z3))
B (SETQ L (CDR L))
(COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
(GO A)))
EXPR)
(DEFPROP INITIALAX1
(LAMBDA(L1)
(PROG (Z L2 L)
(SETQ L L1)
B1 (SETQ L2 L)
A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
(SETQ L2 (CDR L2))
(COND (L2 (GO A1)))
(SETQ L (CDR L))
(COND (L (GO B1)))
(SETQ L L1)
B (SETQ Z (CDDAAR L))
(COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
((NUMBERP (CAAAR L)) NIL)
(T (RPLACA (CAAR L) (CAAAAR L))))
(COND ((ATOM (CDDR Z)) (GO A)))
(RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
A (SETQ L (CDR L))
(COND (L (GO B)))
(RETURN L1)))
EXPR)
(DEFPROP MAPIT
(LAMBDA(X XYZ N)
(PROG (Z Z1 Z2)
(SETQ Z (GETNAME X N))
(COND ((NULL Z) (RETURN NIL)))
A (SETQ ZIN (CAR Z))
(SETQ Z2 (ERRSET (XYZ ZIN) T))
(COND ((NULL Z2) (PRINT (QUOTE SCREWED-FIND)) (RETURN NIL))
((NULL (CAR Z2)) NIL)
(T (SETQ Z1 (CONS (CAR Z) Z1))))
(SETQ Z (CDR Z))
(COND (Z (GO A)))
(RETURN (REVERSE Z1))))
EXPR)
(DEFPROP MATCHER
(LAMBDA(L)
(PROG (FLG Z Z1)
(SETQ Z (EVAL (CADR L)))
(SETQ Z1 (CAR L))
(COND ((ATOM (CADR L))
(COND ((MEMQ (CADR L) (QUOTE (T1 T2 T3 T4))) (SETQ FLG 4))
((MEMQ (CADR L) (QUOTE (L1 L2 L3 L4))) (SETQ FLG 3))
((MEMQ (CADR L) (QUOTE (C))) (SETQ FLG 2) (SETQ Z (CDR Z)))
(T (ERR NIL))))
((EQ (CAADR L) (QUOTE TREE)) (SETQ FLG 1))
(T (ERR NIL)))
(COND ((ATOM Z1) (RETURN (MATCH1 Z1 Z FLG)))
((EQ (CAR Z1) (QUOTE AND)) (GO MAA1))
((EQ (CAR Z1) (QUOTE OR)) (GO MAO1))
(T (RETURN (MATCH1 Z1 Z FLG))))
MAA1 (SETQ Z1 (CDR Z1))
MAAND
(COND ((NULL Z1) (RETURN T)) ((MATCH1 (CAR Z1) Z FLG) (GO MAA1)) (T (RETURN NIL)))
MAO1 (SETQ Z1 (CDR Z1))
MAOR (COND ((NULL Z1) (RETURN NIL)) ((MATCH1 (CAR Z1) Z FLG) (RETURN T)))
(GO MAO1)))
FEXPR)
(DEFPROP MATCH1
(LAMBDA(X Y FL)
(COND ((ATOM X)
(COND ((EQ X (QUOTE %NG)) (COND ((ISLIT FL) (NEG Y)) ((ISCL FL) (MATCHPN Y T)) (T (ERR NIL))))
((EQ X (QUOTE %PL)) (COND ((ISLIT FL) (NOT (NEG Y))) ((ISCL FL) (MATCHPN Y NIL)) (T (ERR NIL))))
((NUMBERP X) (COND ((ISCLS FL) (MATCHTR X Y)) (T (MATMLT X FL))))
((AND (MEMQ X (QUOTE (C1 C2))) (ISCLS FL)) (MEMQ (EVAL X) Y))
(T (ERR NIL))))
((NUMBERP (CAR X)) (COND ((ISCLS FL) (MATCHTR (CAR X) Y)) (T (MATMLT (CAR X) Y FL))))
((EQ (LENGTH X) 1) (MATMLT (CAR X) Y FL))
((ISCLS FL) NIL)
(T (MATMLT* X Y FL))))
EXPR)
(DEFPROP MATCHTR
(LAMBDA (N TR) (MEMQ (CAR (DOWN N CLAUSES)) TR))
EXPR)
(DEFPROP MATCHPN
(LAMBDA(X FL)
(PROG (Z)
A (SETQ Z (NEG (CAR X)))
(COND ((AND Z FL) (RETURN T)) ((AND (NOT Z) (NOT FL)) (RETURN T)))
(SETQ X (CDR X))
(COND (X (GO A)))
(RETURN NIL)))
EXPR)
(DEFPROP MATMLT
(LAMBDA(X Y FL)
(PROG NIL
(COND ((AND (ISTRM FL) (NOT (ASSOC X TBL))) (ERR NIL))
((ISTRM FL) (RETURN (OCR X Y)))
((ISLIT FL) (RETURN (COND ((NEG Y) (OCR X (CDR Y))) (T (OCR X Y))))))
A (COND ((COND ((NEG (CAR Y)) (OCR X (CDAR Y))) (T (OCR X (CAR Y)))) (RETURN T)))
(SETQ Y (CDR Y))
(COND (Y (GO A)))
(RETURN NIL)))
EXPR)
(DEFPROP MATMLT*
(LAMBDA(X Y FL)
(PROG (Z)
(COND ((AND (ISTRM FL) (NOT (ASSOC (CAR X) TBL))) (ERR NIL))
((EQ (CAR X) (QUOTE %NG)) (SETQ X (CDR X)) (GO M1))
((NOT (ISCL FL)) (SETQ Y (LIST Y))))
D (SETQ X (VARIT (LIST X)))
B (SETQ Z (TERMS1 (LIST (COND ((NEG (CAR Y)) (CDAR Y)) (T (CAR Y)))) 64))
A (COND ((UNI X (CAR Z) NIL) (RETURN T)))
(SETQ Z (CDR Z))
(COND (Z (GO A)))
(SETQ Y (CDR Y))
(COND (Y (GO B)))
(RETURN NIL)
M1 (COND ((NEG (CAR Y)) (GO M2)))
M3 (SETQ Y (CDR Y))
(COND (Y (GO M1)))
(RETURN NIL)
M2 (COND ((EQ (LENGTH X) 1) (COND ((EQ (CADAR Y) (CAR X)) (RETURN T)) (T (GO M3)))) (T (GO D)))))
EXPR)
(DEFPROP MAX
(LAMBDA (X Y) (COND ((GREATERP X Y) X) (T Y)))
EXPR)
(DEFPROP MEMC
(LAMBDA(C L)
(PROG NIL
(COND ((NULL L) (RETURN NIL)) ((POS C) (GO A)))
B (COND ((POS (CAR L)) (RETURN NIL)) ((EQUAL C (CAR L)) (RETURN T)))
(SETQ L (CDR L))
(COND (L (GO B)))
(RETURN NIL)
A (COND ((POS (CAR L)) (RETURN (MEMBER C L))))
(SETQ L (CDR L))
(COND (L (GO A)))
(RETURN NIL)))
EXPR)
(DEFPROP MIN1
(LAMBDA(L)
(PROG (Z Z1)
(SETQ Z (CAR L))
M1 (SETQ Z1 (CDR L))
(COND ((NULL Z1)
(COND ((NUMBERP (CAR Z)) (RETURN NIL)) (T (SETQ Z1 (COPY Z)) (RPLACA Z 0) (RETURN Z1))))
((NUMBERP (CAAR Z1)) (GO M2))
((OR (NUMBERP (CAR Z)) (ORDER Z (CAR Z1))) (SETQ Z (CAR Z1))))
M2 (SETQ L (CDR L))
(GO M1)))
EXPR)
(DEFPROP MINIMIZE
(LAMBDA(Z3)
(PROG (Z1 Z2 Z4)
(SETQ Z2 (LIST (CAR Z3)))
ED2 (SETQ Z3 (CDR Z3))
(COND ((NULL Z3) (RETURN (REVERSE Z2))))
(SETQ Z4 (CAR Z3))
(SETQ Z1 Z2)
ED1 (COND ((SUBSUME (CAR Z1) Z4) (GO ED2)))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO ED1)))
(SETQ Z1 (CDR Z3))
ED4 (COND ((NULL Z1) (GO ED5)) ((SUBSUME (CAR Z1) Z4) (GO ED2)))
(SETQ Z1 (CDR Z1))
(GO ED4)
ED5 (SETQ Z2 (CONS Z4 Z2))
(GO ED2)))
EXPR)
(DEFPROP MIN
(LAMBDA (X Y) (COND ((LESSP X Y) X) (T Y)))
EXPR)
(DEFPROP MKSYM
(LAMBDA NIL
(PROG NIL
(SETQ FNLIST (CONS (READLIST (APPEND (EXPLODE FNNAM) (EXPLODE (SETQ FNNO (ADD1 FNNO))))) FNLIST))
(SETQ PREFN (CONS (CAR FNLIST) PREFN))
(RETURN (CAR FNLIST))))
EXPR)
(DEFPROP MODEL
(LAMBDA(C)
(PROG (Z)
(SETQ Z (CDR C))
M1 (COND ((NEG (CAR Z)) (GO M3)) ((MEMBER (CAAR Z) PMODEL) (SETQ SAT C) (RETURN T)))
M2 (SETQ Z (CDR Z))
(COND (Z (GO M1)))
(RETURN NIL)
M3 (COND ((MEMBER (CADAR Z) NMODEL) (SETQ SAT C) (RETURN T)))
(GO M2)))
EXPR)
(DEFPROP NCONC1
(LAMBDA (A B) (COND ((NULL A) B) ((NULL B) A) (T (RPLACD A B))))
EXPR)
(DEFPROP NEGATE
(LAMBDA(Z)
(PROG (BDY)
A (SETQ Z (CDR Z))
(COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
(SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
(SETQ Z (CDDR Z))
C (COND ((NULL Z) (GO D)))
(SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
(SETQ Z (CDR Z))
(GO C)
D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
EXPR)
(DEFPROP NEGSGN
(NIL . ¬)
VALUE)
(DEFPROP NOSYM
(LAMBDA (L) (COND ((NULL L) 0) ((ATOM L) 1) (T (MAX (ADD1 (NOSYM (CAR L))) (NOSYM (CDR L))))))
EXPR)
(DEFPROP OCR
(LAMBDA (X Y) (OCR1 X (LIST Y)))
EXPR)
(DEFPROP OCR1
(LAMBDA(X Y)
(COND ((NULL Y) NIL)
((VAR (CAR Y)) (OCR1 X (CDR Y)))
((CONST (CAR Y)) (COND ((EQ (CAAR Y) X) T) (T (OCR1 X (CDR Y)))))
((EQ X (CAAR Y)) T)
((OCR1 X (CDAR Y)) T)
(T (OCR1 X (CDR Y)))))
EXPR)
(DEFPROP ONEGSGN
(NIL . ¬)
VALUE)
(DEFPROP *NOPOINT
(NIL . T)
VALUE)
(DEFPROP OCCUR
(LAMBDA(X Z)
(PROG (Z1)
OC1 (SETQ Z1 (CAR Z))
(COND ((VAR Z1) (COND ((EQ X Z1) (RETURN T)) (T (GO OC2))))
((CONST Z1) (GO OC2))
((OCCUR X (CDR Z1)) (RETURN T)))
OC2 (SETQ Z (CDR Z))
(COND (Z (GO OC1)))
(RETURN NIL)))
EXPR)
(DEFPROP ORDER
(LAMBDA(X Y)
(COND ((POS X) (COND ((POS Y) (ORDERP (CAR X) (CAR Y))) (T T)))
((NEG X) (COND ((NEG Y) (ORDERP (CADR X) (CADR Y))) (T NIL)))))
EXPR)
(DEFPROP ORDEREQUAL
(LAMBDA(S)
(PROG NIL
(COND ((VAR (CAR S))
(COND ((VAR (CADR S)) (COND ((GREATERP (CADR S) (CAR S)) (GO A)) (T (RETURN NIL)))) (T (GO A))))
((CONST (CAR S))
(COND ((VAR (CADR S)) (RETURN NIL))
((CONST (CADR S)) (COND ((ORDERP (CAAR S) (CAADR S)) (GO A)) (T (RETURN NIL))))
(T (GO A))))
((OR (VAR (CADR S)) (CONST (CADR S))) (RETURN NIL))
((GREATERP (DEPTH1 (CDAR S)) (DEPTH1 (CDADR S))) (RETURN NIL)))
A (PROG (S1) (SETQ S1 (CADR S)) (RPLACA (CDR S) (CAR S)) (RPLACA S S1))))
EXPR)
(DEFPROP PARMOD
(LAMBDA(C D)
(COND ((ALLNEG C) (PARMOD1 D C)) ((ALLNEG D) (PARMOD1 C D)) (T (NCONC (PARMOD1 C D) (PARMOD1 D C)))))
EXPR)
(DEFPROP PARMOD1
(LAMBDA(C D)
(PROG (YC YD Z Z1 Z2 X Y Y1 Y2 PAR TS)
(COND ((EQ C D) (RETURN NIL)))
(SETQ YC (CDR C))
PAR1 (SETQ YD (CDR D))
(SETQ X (CAR YC))
(COND ((NEG X) (RETURN PAR))
((ORDERP (CAR X) EQUAL) (GO PAR2))
((NOT (EQ (CAR X) EQUAL)) (RETURN PAR)))
PAR3 PAR3A
(COND ((NEG (CAR YD)) (SETQ Z2 (CDAR YD))) (T (SETQ Z2 (CAR YD))))
(SETQ Y1 (CDR X))
(COND ((VAR (CAR Y1)) (GO PAR7A)))
(SETQ Y2 (CADR Y1))
(SETQ Z (TERMS (CAAR Y1) (CDR Z2) PDEPTH))
(COND ((NULL Z) (GO PAR7A)))
PAR5 (SETQ Z1 Z)
PAR4 (SETQ Y (UNIFY (LIST (CAR Y1)) (LIST (CAAR Z1))))
(COND (Y (GO PAR6)))
PAR7 (SETQ Z1 (CDR Z1))
(COND (Z1 (GO PAR4)))
PAR7A
(SETQ YD (CDR YD))
(COND (YD (GO PAR3A)))
PAR2 (SETQ YC (CDR YC))
(COND (YC (GO PAR1)))
(RETURN PAR)
PAR6 (SETQ TS (CADR (SUBS3T* (CDR Y) (LIST NIL Y2))))
PAR9 (SETQ PARRES (SUBS3TA (CDR Y) Z2 (CAR Z1) TS))
(COND ((NEG (CAR YD)) (SETQ PARRES (CONS ESCAPE PARRES))))
(SETQ Y (UNION (CDR Y) C D X (CAR YD)))
(COND ((NULL Y) (GO PAR7)))
(SETQ PAR (CONS (SET2 (CAR (COND (DLIST (DEMOD Y DLIST)) (T Y))) TBL) PAR))
(GO PAR7)))
EXPR)
(DEFPROP POTZ
(LAMBDA(X)
(PROG (Z Z1)
(SETQ Z (POTZ1 X))
(COND ((SETQ Z1 (PMEMQ Z POTZTBL)) (RETURN Z1)))
(SETQ POTZTBL (CONS Z POTZTBL))
(RETURN Z)))
EXPR)
(DEFPROP PRECNF
(LAMBDA(X)
(COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
((EQ (CAR X) (QUOTE EQUIV))
(LIST (QUOTE AND)
(LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
(LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
(T X)))
EXPR)
(DEFPROP PROOF1
(LAMBDA(L)
(PROG (Q X Y Z P P1)
(PRINC (QUOTE / ))
(PRINC (QUOTE / ))
(PRFPRINT (CDR L))
(SETQ P (ANCESTOR L))
(COND ((ATOM (CDR P)) (GO P3)))
(SETQ P1 (CDR P))
(SETQ P (CAR P))
(PRINC (QUOTE / ))
(PRINC 1)
(PRINC (QUOTE / ))
(PRINC 2)
(SETQ X 1)
(SETQ Y 2)
(SETQ Q (LIST (CONS X P) (CONS Y P1)))
P1 (SETQ Z (ANCESTOR (CDAR Q)))
(COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
(SETQ X (ADD1 Y))
(SETQ Y (ADD1 X))
(PRINT (CAAR Q))
(PRFPRINT (CDDAR Q))
(PRINC X)
(PRINC (QUOTE / ))
(PRINC Y)
(SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
P2 (SETQ Q (CDR Q))
(COND ((NULL Q) (RETURN NIL)))
(GO P1)
P3 (PRIN1 (CDR P))
(RETURN (TERPRI))))
EXPR)
(DEFPROP PROVE
(LAMBDA (L) (PROG (AUTO) (SETQ AUTO T) (EVAL (CONS (QUOTE TRY1) L))))
FEXPR)
(DEFPROP PRPAR
(LAMBDA(L)
(PROG NIL
(CLAUSES CLAUSES)
(TERPRI)
P1 (PROOF1 (CAR L))
(TERPRI)
(TERPRI)
(SETQ L (CDR L))
(COND (L (GO P1)))
(RETURN NIL)))
EXPR)
(DEFPROP PRFPRINT
(LAMBDA(X)
(PROG NIL
(SETQ &&Z (FUNFLAT (LIST (LIST (OUTTST (CNVT X) (FUNCTION >S<))))))
(SETQ LAST NIL)
(FPRINT &&Z 0)))
EXPR)
(DEFPROP PRFPR1
(LAMBDA(L)
(PROG (Z)
(COND ((NEG L) (PRINC ONEGSGN) (SETQ L (CDR L))))
(PRINC (CAR L))
(SETQ L (CDR L))
(PRINC (QUOTE /())
P1 (COND ((VAR (CAR L))
(COND ((MINUSP (CAR L)) (PRINC (QUOTE Z)) (PRINC (MINUS (CAR L))))
(T (PRINC (QUOTE X))
(COND ((SETQ Z (ASSOC (CAR L) VARL)) (PRINC (CDR Z)))
(T (SETQ VARL (CONS (CONS (CAR L) (SETQ ONO (ADD1 ONO))) VARL)) (PRINC ONO))))))
((CONST (CAR L)) (PRINC (CAAR L)))
(T (PRFPR1 (CAR L))))
P2 (SETQ L (CDR L))
(COND ((NULL L) (PRINC (QUOTE /))) (RETURN NIL)))
(PRINC (QUOTE /,))
(GO P1)))
EXPR)
(DEFPROP PROOF
(LAMBDA(L R)
(PROG (Q Q1 X Z)
(SETQ LHP L)
(SETQ RHP R)
(RPLACA (MKWRD L) 1)
(RPLACA (MKWRD R) 2)
(SETQ X 2)
(SETQ Q (LIST L R))
(SETQ Q1 Q)
P1 (SETQ Z (ANCESTOR (CAR Q)))
(COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
(RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
(RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
(NCONC Q (LIST (CAR Z) (CDR Z)))
P2 (SETQ Q (CDR Q))
(COND (Q (GO P1)))
(PRINT (QUOTE NIL))
(PRINC (CAR (MKWRD (CAR Q1))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CADR Q1))))
(SETQ X 1)
A (COND
((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
(PRFPRINT (CDAR Q1))
(COND
((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
((ATOM (CDR (ANCESTOR (CAR Q1))))
(PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
(T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
(SETQ Q1 (CDR Q1))
(SETQ X (ADD1 X))
(COND (Q1 (GO A)))))
EXPR)
(DEFPROP PTRS
(LAMBDA(X)
(PROG (Z)
A (COND ((VAR (CAAR X)) NIL) ((CONST (CAAR X)) NIL) (T (SETQ Z (APPEND (TCOPY (CDAAR X)) Z))))
(SETQ X (CDR X))
(COND (X (GO A)))
(RETURN Z)))
EXPR)
(DEFPROP QUERY
(LAMBDA NIL
(PROG NIL
(COND (STRATEGY (PRINT (QUOTE CHOICE-STRATEGY-IS:)) (OUT >ST< (CAR (LAST STRATEGY)))))
(PRINT (QUOTE EDIT-STRATEGY-IS:))
(OUT >ST< (CAR (LAST EDITSTRAT)))
(COND ((AND (NULL PMODEL) (NULL NMODEL)) (GRINDEF MODEL))
(T (PRINT (QUOTE POSITIVE-MODEL=))
(PRINC PMODEL)
(PRINT (QUOTE NEGATIVE-MODEL=))
(PRINC NMODEL)))
(PRINT (QUOTE PARMODULATE))
(PRINC (QUOTE =))
(COND ((NOT PFLG) (PRINC T)
(PRINT (QUOTE EQUAL-SYMBOL))
(PRINC (QUOTE =))
(PRINC EQUAL)
(PRINT (QUOTE PAR-DEPTH-BOUND))
(PRINC (QUOTE =))
(PRINC PDEPTH))
(T (PRINC NIL)))
(PRINT (QUOTE ELAPSED-TIME))
(PRINC (QUOTE =))
(PRINC (TIMEIT))
(RETURN (TERPRI))))
EXPR)
(DEFPROP REAL-LNGTH
(LAMBDA(L)
(PROG (N)
(SETQ N 0)
A (COND ((NULL (CDR L)) (RETURN N)) ((HERE (CAR L)) (SETQ N (ADD1 N))))
(SETQ L (CDR L))
(GO A)))
EXPR)
(DEFPROP REDUCER
(LAMBDA(C L)
(PROG (Z Z1 Z2 Z3 C1)
(SETQ Z (CDAR C))
(SETQ Z2 (CDAAR C))
(SETQ C1 C)
(SETQ Z3 (SETQ Z1 (CONS NIL (CAR Z2))))
A (COND ((EQ L (CDR C1)) (GO B)))
(SETQ C1 (CDR C1))
(SETQ Z1 (CDR Z1))
(GO A)
B (RPLACD C1 (CDDR C1))
(COND ((EQ (CAR Z) L) (RPLACA Z (CDR L))))
(COND ((EQ (CDR Z2) (CDR Z1)) (RPLACD Z2 (CDDR Z2))))
(RPLACD Z1 (CDDR Z1))
(RPLACA Z2 (CDR Z3))
(RPLACA (CAAR C) (SUB1 (CAAAR C)))
(RETURN C)))
EXPR)
(DEFPROP REENTER
(LAMBDA NIL (PROG NIL (ATTEMPT1 XYZ2) (RETURN NIL)))
EXPR)
(DEFPROP RESTORE
(LAMBDA(IL)
(PROG (ZZ) (EVAL (CONS (QUOTE INPUT) IL)) (INC T) (SETQ ZZ (RESTORE1 (READ))) (INC NIL) (RETURN (SET3 ZZ))))
FEXPR)
(DEFPROP RESTORE1
(LAMBDA(L)
(PROG (Z2 Z L1 L2 Z1 N)
(SETQ L1 L)
(SETQ N 0)
D (SETQ L2 (CONS (CONS N (CAR L)) L2))
(SETQ L (CDR L))
(SETQ N (ADD1 N))
(COND (L (GO D)))
(SETQ L L1)
E (SETQ Z (CAAR L1))
(SETQ Z1 (CADR Z))
(COND ((NULL Z1) (GO A)))
(SETQ Z2 (CDAR L1))
B (COND ((ZEROP Z1) (RPLACA (CDR Z) Z2) (GO A)))
(SETQ Z1 (SUB1 Z1))
(SETQ Z2 (CDR Z2))
(GO B)
A (SETQ Z1 (CDDDR Z))
(COND ((NULL (CDR Z1)) (RPLACD (CDDR Z) (CAR Z1)) (GO C)) ((NULL (CAR Z1)) (SETQ Z1 (CDR Z1))))
F (RPLACA Z1 (CDR (ASSOC (CAR Z1) L2)))
(RPLACD Z1 (CDR (ASSOC (CDR Z1) L2)))
C (SETQ L1 (CDR L1))
(COND (L1 (GO E)))
(RETURN L)))
EXPR)
(DEFPROP RESOLVE
(LAMBDA(C D)
(COND ((OR (ALLNEG D) (ALLPOS C)) (RESOLVE1 C D))
((OR (ALLPOS D) (ALLNEG C)) (RESOLVE1 D C))
(T (NCONC (RESOLVE1 C D) (RESOLVE1 D C)))))
EXPR)
(DEFPROP RESTS
(LAMBDA(L)
(PROG (Z Z1)
A (COND ((ATOM (CAR L)) (SETQ Z (CONS (CAR L) Z)))
((EQ (LENGTH (CAR L)) 1) (RETURN NIL))
(T (SETQ Z1 T) (SETQ Z (CONS (CDAR L) Z))))
(SETQ L (CDR L))
(COND (L (GO A)) ((NULL Z1) (RETURN NIL)))
(RETURN (REVERSE Z))))
EXPR)
(DEFPROP RESOLVE1
(LAMBDA(C D)
(PROG (CB DB DB1 YC YD YD1 Z X Y RES)
(COND ((AND COND (EVAL COND)) (ERR (CDR LCL))))
(SETQ YC (CDR C))
(SETQ CB (POSBIT C))
(SETQ YD1 (NEGL D))
(SETQ DB1 (NEGBIT D))
(SETQ DB DB1)
(SETQ YD YD1)
RES1 (SETQ X (CAR YC))
(COND ((NEG X) (RETURN RES)))
(SETQ Y (CAR YD))
(COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
(SETQ YD1 YD)
(SETQ DB1 DB)
(GO RES2A)
RES2 (SETQ Y (CAR YD))
(COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
RES2A
(COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
(SETQ Z (UNIFY (CDR X) (CDDR Y)))
(COND ((NULL Z) (GO RES2B)))
(SETQ PARRES NIL)
(SETQ Z (UNION (CDR Z) C D X Y))
(COND ((NULL Z) (GO RES2B)) ((NULL (CAR Z)) (RETURN Z)))
(SETQ RES (CONS (SET2 (CAR (COND (DLIST (DEMOD Z DLIST)) (T Z))) TBL) RES))
RES2B
(SETQ YD (CDR YD))
(COND (YD (SETQ DB (CDR DB)) (GO RES2)))
RES3A
(SETQ DB DB1)
(SETQ YD YD1)
RES3 (SETQ YC (CDR YC))
(COND (YC (SETQ CB (CDR CB)) (GO RES1)))
(RETURN RES)
RES4 (SETQ YD (CDR YD))
(COND (YD (SETQ DB (CDR DB)) (GO RES1)))
(GO RES3A)))
EXPR)
(DEFPROP RESTART
(LAMBDA(X)
(PROG (ZZ TIME1)
(EVAL (CONS (QUOTE INPUT) X))
(INC T)
(SETQ ZZ (RESTORE1 (READ)))
(SETQ STRAT (READ))
(SETQ COND (READ))
(INC NIL)
(SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
(RETURN (ATTEMPT (CONS ZZ (FIXSET ZZ)) STRAT COND))))
FEXPR)
(DEFPROP RESET
(LAMBDA(L)
(PROG (Z) R1 (SETQ Z (EVAL (CONS (QUOTE RESET1) (CAR L)))) (SETQ L (CDR L)) (COND (L (GO R1))) (RETURN Z)))
FEXPR)
(DEFPROP RESET1
(LAMBDA(L)
(PROG (X Z2 Z3 ZZ XX Z Z1 F1)
(SETQ Z STATEVECTOR)
A (COND
((EQ (CAR L) (CAR Z)) (SETQ F1 T)
(COND ((EQ (CAR L) (QUOTE STRATEGY)) (GO R1))
(T (SET (CAR Z) (EVAL (CADR L)))))))
R2 (SETQ Z1 (CONS (EVAL (CAR Z)) Z1))
(SETQ Z (CDR Z))
(COND (Z (GO A)))
(COND (F1 (RETURN (REVERSE Z1))))
R3 (PRINT (QUOTE UNDEFINED-ARG-FOR-RESET:))
(PRINC (CAR L))
(TERPRI)
(ERR NIL)
R1 (SETQ X (QUOTE (X)))
(SETQ L (CDR L))
R4 (SETQ Z2 (CAR L))
(COND ((ATOM Z2) (SETQ Z3 Z2)) (T (SETQ Z3 (CAR Z2))))
SPQ2 (COND ((NOT (MEMQ Z3 STRATLIST)) (GO R3))
((EQ Z3 (QUOTE SUPPORT)) (SETQ XX (EVAL (CADAR L)))
(PROG (ZZ)
(GO B)
A (SETQ ZZ (CONS (CDAR XX) ZZ))
(SETQ XX (CDR XX))
B (COND (XX (GO A)))
(SETQ SUPPORT ZZ))
(SETQ ZZ (QUOTE (SUPPORT C2))))
((EQ Z3 (QUOTE MODEL)) (SETQ PMODEL (CADAR L))
(SETQ NMODEL (CADDAR L))
(SETQ ZZ (CONS (CONS Z3 X) ZZ)))
((EQ Z3 (QUOTE ANCESTRY)) (SETQ ANCESTRY T))
((EQ Z3 (QUOTE ORDER)) (SETQ ORDER T))
((EQ Z3 (QUOTE MERGE)) (SETQ MERGE T))
(T (SETQ ZZ (CONS (CONS Z3 X) ZZ))))
(SETQ L (CDR L))
(COND (L (GO R4)))
(COND (ZZ (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))) (T (SETQ STRATEGY NIL)))
(GO R2)))
FEXPR)
(DEFPROP SAVE
(LAMBDA(CL)
(PROG (L)
(SETQ L (SAVE1 (EVAL (CADDR CL))))
(EVAL (CONS (QUOTE OUTPUT) (LIST (CAR CL) (CADR CL))))
(OUTC T T)
(PRINT L)
(PRINT STRAT)
(PRINT COND)
(OUTC NIL T)
(RETURN NIL)))
FEXPR)
(DEFPROP SAVE1
(LAMBDA(L)
(PROG (L1 N ASLST CLST Z Z2 Z3 Z4 Z5)
(SETQ N 0)
(SETQ Z L)
A (SETQ ASLST (CONS (CONS (CAR L) N) ASLST))
(SETQ L (CDR L))
(SETQ N (ADD1 N))
(COND (L (GO A)))
(SETQ CLST (LAST Z))
(SETQ L Z)
B (SETQ Z2 (CAAR L))
(COND ((NULL (CAR Z2)) (SETQ Z3 NIL)) (T (SETQ Z3 (CAAR Z2))))
(COND ((NULL (CADR Z2)) (SETQ Z4 NIL))
(T
(SETQ Z4
(PROG (Z Z1 N)
(SETQ N 0)
(SETQ Z1 (CDAR L))
(SETQ Z (CADR Z2))
A (COND ((EQ Z Z1) (RETURN N)))
(SETQ Z1 (CDR Z1))
(SETQ N (ADD1 N))
(GO A)))))
(SETQ Z (CDDDR Z2))
(COND ((ATOM (CDR Z))
(COND ((NOT (ATOM (CAR Z))) (SETQ Z5 (UNWIND (CAAR Z) (CDAR Z) CLST ASLST N))
(SETQ N (CDR Z5))
(SETQ Z5 (CONS NIL (CAR Z5))))
(T (SETQ Z5 (LIST Z)))))
(T (SETQ Z2 (UNWIND (CAR Z) (CDR Z) CLST ASLST N)) (SETQ Z5 (CAR Z2)) (SETQ N (CDR Z2))))
(SETQ Z (CONS Z3 (CONS Z4 (CONS 0 Z5))))
(SETQ L1 (CONS (CONS Z (CDAR L)) L1))
C (SETQ L (CDR L))
(COND (L (GO B)))
(RPLACD CLST NIL)
(RETURN (REVERSE L1))))
EXPR)
(DEFPROP SET1
(LAMBDA(L)
(PROG (TBL N)
(SETQ N 1)
(SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
(SETQ L (CDR L))
(COND (L (SETQ N (ADD1 N)) (GO A)))
(RETURN (SETU TBL))))
EXPR)
(DEFPROP SET2
(LAMBDA(C L)
(PROG (X Z T1 T2 T3* T2* T3 Z1)
(SETQ T2 (SETQ T2* (LIST NIL)))
(SETQ T3 (SETQ T3* (LIST NIL)))
(SETQ X (CDR C))
S1 (SETQ Z (CDAR X))
(SETQ T1 NIL)
(COND ((NEG (CAR X)) (GO S2)))
S1A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
(T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
(SETQ T1 (CONS (CDAR (LAST L)) T1))))
(SETQ Z (CDR Z))
(COND (Z (GO S1A)))
(SETQ X (CDR X))
(RPLACD T2* (LIST (POTZ T1)))
(SETQ T2* (CDR T2*))
(COND (X (GO S1)))
S4 (COND ((EQ T2 T2*) (RPLACA T3 (CDR T3))) (T (RPLACA T3 (CDR T2)) (RPLACD T2* (CDR T3))))
(RPLACA (CAR C) (CONS (CAAR C) T3))
(RETURN C)
S2 (SETQ Z (CDDAR X))
(SETQ T1 NIL)
S2A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
(T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
(SETQ T1 (CONS (CDAR (LAST L)) T1))))
(SETQ Z (CDR Z))
(COND (Z (GO S2A)))
(SETQ X (CDR X))
(RPLACD T3* (LIST (POTZ T1)))
(SETQ T3* (CDR T3*))
(COND (X (GO S2)))
(GO S4)))
EXPR)
(DEFPROP SET3
(LAMBDA(Z)
(PROG (E)
(COND ((OR (NULL Z) (MEMQ NIL Z)) (RETURN Z)))
(SETQ E Z)
S1 (COND ((HERE (CAR E)) (SET2 (CAR E) TBL)))
(SETQ E (CDR E))
(COND (E (GO S1)))
(RETURN Z)))
EXPR)
(DEFPROP SETUP
(LAMBDA(Z)
(PROG (BL Z1 Z2 Z3 Z4 Z5)
SET2 (SETQ Z3 (CAR Z))
(SETQ Z2 0)
(SETQ BL NIL)
(SETQ NO* NO)
(SETQ Z5 NIL)
S1 (SETQ Z4 (MIN1 Z3))
(COND ((NULL Z4) (GO S3)))
(UPIT Z4)
(COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
(SETQ Z2 (ADD1 Z2))
(SETQ Z5 (CONS Z4 Z5))
(GO S1)
S3 (SETQ Z3 NIL)
(SETQ Z4 Z5)
S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
(SETQ Z4 (CDR Z4))
(COND (Z4 (GO S2)))
SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
SET1 (SETQ Z1 (CONS Z5 Z1))
S4 (SETQ Z (CDR Z))
(COND (Z (GO SET2)))
(RETURN Z1)))
EXPR)
(DEFPROP SEARCH2
(LAMBDA (X L L1) (PROG NIL (SETQ KR1 (ASSOC X L)) (COND (KR1 (RETURN (CDR KR1)))) (RETURN L1)))
EXPR)
(DEFPROP S2
(LAMBDA(X Y Z)
(PROG (Z1)
(SETQ Z1 (CDR Z))
A (COND ((NULL Z1) (RETURN Z))
((VAR (CAR Z1)) (COND ((EQ (CAR Z1) Y) (RPLACA Z1 X))))
((CONST (CAR Z1)) NIL)
(T (RPLACA Z1 (S2 X Y (CAR Z1)))))
(SETQ Z1 (CDR Z1))
(GO A)))
EXPR)
(DEFPROP SETQUERY
(LAMBDA (X) (SETQUERY2 X NIL NIL))
EXPR)
(DEFPROP SETQUERY1
(LAMBDA(XYZ XYZ1)
(PROG (Z)
(SETQ Z (ERRSET (SETQUERY2 XYZ XYZ1 T)))
(COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
(RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
EXPR)
(DEFPROP SETQUERY2
(LAMBDA(XX YY FLG)
(PROG (XYZ1 N
CHAN
Z
Z1
Z3
XYZ
Z6
SUPPORT
EDITSTRAT
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
STRATEGY
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST)
(SETQ CHAN (OUTC NIL NIL))
(COND (FLG (UPDATESTATE YY)))
(SETQ XYZ1 XX)
(COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
(PRINT SETQMESS)
(SETQ XX (UPDATE XX))
(SETQ XYZ1 XX)
SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
(PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
(SETQ N 1)
AA (UP1B (CAR XX) N)
(SETQ N (ADD1 N))
(SETQ XX (CDR XX))
(COND (XX (GO AA)))
SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
(AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
(COND
((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
SRA2 (PRINT (QUOTE DOIT-CHOICE-STRATEGY))
(SCANSET)
(START)
(SETQ Z (ERRSET (<ST>) T))
(SCANRESET)
(COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SRA2)))
(SETQ ZIN (TOP))
(SETQ STRATEGY (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) ZIN))
(OUT >ST< ZIN)
SRB (PRINT (QUOTE DEBUG))
(PRINC (QUOTE =))
(COND (FLG (RESTRAT DEBUG SRA SRAA) (PRINC DEBUG) (BARF NIL) (RESTRAT2 DEBUG SRA))
(T (RESTRATS DEBUG SRA)))
SRAA SRC
SRD (PRINT (QUOTE DOIT-EDIT-STRATEGY))
(SCANSET)
(START)
(SETQ Z1 (ERRSET (<ST>) T))
(SCANRESET)
(COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
(SETQ ZIN (TOP))
(SETQ EDITSTRAT (LIST (QUOTE LAMBDA) (QUOTE (C)) ZIN))
(OUT >ST< ZIN)
SRCA SRI
(PRINT (QUOTE (UNIT-REDUCTION (Y / N))))
(COND (FLG (RESTRAT UFLG SRD SRIA) (PRINC UFLG) (BARF NIL) (RESTRAT2 UFLG SRC))
(T (RESTRATS UFLG SRD)))
SRIA SRE
(PRINT (QUOTE PARAMODULATE))
(COND (FLG (PRINC (QUOTE IS))
(PRINC (QUOTE / ))
(COND (PFLG (PRINC (QUOTE N))) (T (PRINC (QUOTE Y))))
(PRINT (QUOTE (DO YOU WANT TO PARAMODULATE (Y / N))))
(SETQ Z3 (READ))
(COND ((EQ Z3 (QUOTE Y)) (SETQ PFLG NIL) (GO SRDA))
((EQ Z3 (QUOTE N)) (GO SPQ5))
((EQ Z3 ESCAPE) (PRINT (QUOTE RESETTING-TO:)) (GO SRI))
(T (GO SRE))))
(T (PRINC (QUOTE (Y / N)))
(RESTRATS Z3 SRI)
(SETQ EQUAL ESCAPE)
(COND ((EQ Z3 (QUOTE N)) (GO SPQ5)))))
SRDA (SETQ AXNO 1)
SRF (PRINT (QUOTE EQUAL-SYMBOL))
(PRINC (QUOTE =))
(COND (FLG (RESTRAT EQUAL SRE SREA) (PRINC EQUAL) (BARF NIL) (RESTRAT2 EQUAL SRE))
(T (RESTRATS EQUAL SRE)))
SREA (SETQ PFLG NIL)
SRG (PRINT (QUOTE PAR-DEPTH-BOUND))
(PRINC (QUOTE =))
(COND (FLG (RESTRAT PDEPTH SRF SRFA) (PRINC PDEPTH) (BARF NIL) (RESTRAT2 PDEPTH SRF))
(T (RESTRATS PDEPTH SRF)))
SRFA P1
(PRINT (QUOTE DEMODULATION-LIST))
(PRINC (QUOTE =))
(PRINT (QUOTE (TYPE: 'NONE' OR 'IN' (TO INSERT))))
(COND (FLG (RESTRAT XYZ SRH SRHA) (PRINC XYZ) (BARF NIL) (RESTRAT2 XYZ SRH)) (T (RESTRATS XYZ SRG)))
SRHA (SETQ DLIST NIL)
(COND ((EQ XYZ (QUOTE NONE)) (GO SPQ6))
((EQ XYZ (QUOTE IN)) (GO P2))
(T (PRINT (QUOTE UNDEFINED-SPECIFICATION-FOR-DEMOD-LIST))))
(GO P1)
P2 (SETQ Z3 (INCLAUSES))
P2A (COND ((NULL Z3) (PRINT (QUOTE ERROR-TRY-AGAIN)) (GO P1)))
P3 (SET3 (SETQ DLIST Z3))
SRH (PRINT (QUOTE DEMOD-DEPTH-BOUND=))
(COND (FLG (RESTRAT DDEPTH P1 SRGA) (PRINC DDEPTH) (BARF NIL) (RESTRAT2 DDEPTH P1))
(T (RESTRATS DDEPTH P1)))
SRGA P6
(GO SPQ6)
SPQ5 (SETQ PFLG T)
SPQ6 (SETQ Z1
(LIST STRATEGY
SUPPORT
EDITSTRAT
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST))
(OUTC CHAN NIL)
(COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
EXPR)
(DEFPROP SUBS3TA
(LAMBDA(L Z XX TS)
(PROG (X1 X2 X3 Z4)
(SETQ X1 (LIST (CAR Z)))
(SETQ X2 X1)
(GO SUB2)
SUB1 (RPLACD X2 (LIST X3))
(SETQ X2 (CDR X2))
SUB2 (SETQ Z (CDR Z))
(SETQ Z4 (CAR Z))
(COND ((NULL Z) (RETURN X1))
((EQ Z XX) (SETQ X3 TS) (GO SUB1))
((VAR Z4) (SETQ X3 (SEARCH Z4 L)) (GO SUB1))
((CONST Z4) (SETQ X3 Z4) (GO SUB1))
(T (SETQ X3 (SUBS3TA L Z4 XX TS)) (GO SUB1)))))
EXPR)
(DEFPROP SUBS3T**
(LAMBDA (L X) (COND ((NULL L) (SUBS3T (QUOTE ((-11 . -1))) X)) (T (SUBS3T L X))))
EXPR)
(DEFPROP SUB*
(LAMBDA(X L)
(PROG (S2 Z L1)
B (SETQ L1 L)
A (SETQ S2 (CDADAR L1))
(SETQ Z (UNI (LIST (CAR S2)) (LIST (CAAR X)) NIL))
(COND (Z (RPLACA (CAR X) (CADR (SUBS3T* Z (CONS NIL (CDR S2)))))))
(SETQ L1 (CDR L1))
(COND (L1 (GO A)))
(SETQ X (CDR X))
(COND (X (GO B)))))
EXPR)
(DEFPROP SUBSKOL
(LAMBDA (C EXL) (SUBS3T EXL C))
EXPR)
(DEFPROP SUPPORT
(LAMBDA (X) (PROG NIL (COND ((NOT (EQ LVL 1)) (RETURN T)) (T (RETURN (MEMBER (CDR X) SUPPORT))))))
EXPR)
(DEFPROP SUBSUME1
(LAMBDA(C CB D DB L)
(PROG (Z)
SUB5 (COND ((NEG (CAR C)) (GO SUB3))
((NEG (CAR D)) (RETURN NIL))
((EQ (CAAR C) (CAAR D)) (GO SUB1))
((ORDERP (CAAR C) (CAAR D)) (RETURN NIL))
(T (GO SUB2)))
SUB1 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDAR C) (CDAR D) L))) (T (GO SUB2)))
SUB4 (COND ((NULL Z) (GO SUB2)) ((NULL (CDR C)) (RETURN T)) ((SUBSUME1 (CDR C) (CDR CB) D DB Z) (RETURN T)))
SUB2 (SETQ D (CDR D))
(COND (D (SETQ DB (CDR DB)) (GO SUB5)))
(RETURN NIL)
SUB3 (COND
((NEG (CAR D))
(COND ((EQ (CADAR C) (CADAR D))
(COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDDAR C) (CDDAR D) L)) (GO SUB4))
(T (GO SUB2))))
((ORDERP (CADAR C) (CADAR D)) (RETURN NIL))
(T (GO SUB2)))))
(SETQ D (CDR D))
(COND (D (SETQ DB (CDR DB)) (GO SUB3)))
(RETURN NIL)))
EXPR)
(DEFPROP SUBS2T
(LAMBDA(X Y Z)
(PROG (U Z1)
(COND ((EQ X Y) (RETURN Z)))
(SETQ U (CDR Z))
(GO S2)
S1 (SETQ Z1 (CDAR U))
(COND ((VAR Z1) (COND ((EQ Y Z1) (RPLACD (CAR U) X))))
((CONST Z1) NIL)
(T (RPLACD (CAR U) (S2 X Y Z1))))
(SETQ U (CDR U))
S2 (COND (U (GO S1)))
(RPLACD Z (CONS (CONS Y (COND ((OR (VAR X) (CONST X)) X) (T (COPY X)))) (CDR Z)))
(RETURN Z)))
EXPR)
(DEFPROP SUBS3T
(LAMBDA (L X) (COND ((NEG X) (CONS ESCAPE (SUBS3T* L (CDR X)))) (T (SUBS3T* L X))))
EXPR)
(DEFPROP SUBSUME
(LAMBDA(C D)
(COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
(T NIL)))
EXPR)
(DEFPROP SUBSUME*
(LAMBDA (C D) (PROG NIL (RETURN (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))))
EXPR)
(DEFPROP SUBST1
(LAMBDA(X Y Z)
(COND ((ATOM Z) (COND ((EQ Y Z) X) (T Z)))
((EQUAL Y Z) X)
(T (CONS (SUBST1 X Y (CAR Z)) (SUBST1 X Y (CDR Z))))))
EXPR)
(DEFPROP TCOPY
(LAMBDA (X) (COND ((NULL X) NIL) ((VAR (CAR X)) (TCOPY (CDR X))) (T (CONS X (TCOPY (CDR X))))))
EXPR)
(DEFPROP TEMPLATE
(LAMBDA(L)
(PROG (NAME VARLIS Z Z1 Z2)
(SETQ NAME (CAR L))
(SETQ L (CADR L))
(COND ((NOT (EQ (CAR L) (QUOTE LAMBDA))) (PRINT (QUOTE ERROR))))
(SETQ VARLIS (CADR L))
(SETQ L (CDDR L))
P1 (COND ((NULL L) (GO P3)))
(SETQ Z (MKPRED L))
P2 (COND
(Z (COND ((ATOM (CAAR Z)) (SETQ Z1 (NCONC Z1 (LIST Z)))) (T (SETQ Z1 (NCONC Z1 Z))))
(SETQ L (CDDR L))
(GO P1)))
(SETQ L (CDR L))
(COND ((NULL L) (GO P3)))
(SETQ Z (MKPRED L))
(SETQ Z2 (NCONC Z2 (LIST Z1)))
(SETQ Z1 NIL)
(COND (Z (GO P2)))
P3 (PUTPROP NAME (QUOTE (LAMBDA (L) (CONS (QUOTE APPLYTEMP) L))) (QUOTE MACRO))
(SETQ TEMPLATELIST (CONS (CONS NAME (CONS VARLIS Z2)) TEMPLATELIST))))
FEXPR)
(DEFPROP TERMS
(LAMBDA (X Y Z) (CDR (TERMS2 X Y Z)))
EXPR)
(DEFPROP TERMS1
(LAMBDA(L N)
(COND ((OR (ZEROP N) (NULL L)) NIL)
((OR (VAR (CAR L)) (CONST (CAR L))) (CONS L (TERMS1 (CDR L) N)))
(T (NCONC (LIST L) (TERMS1 (CDAR L) (SUB1 N)) (TERMS1 (CDR L) (SUB1 N))))))
EXPR)
(DEFPROP TERMS2
(LAMBDA(Z L N)
(PROG (Z1 T1 T2)
(SETQ T2 (SETQ T1 (LIST NIL)))
A (COND ((NULL L) (RETURN T1))
((VAR (CAR L)) (GO B))
((CONST (CAR L)) (COND ((EQ Z (CAAR L)) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2)))) (GO B))
((EQ N 1) (GO B)))
(SETQ Z1 (TERMS2 Z (CDAR L) (SUB1 N)))
(COND ((EQ (CAAR L) Z) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2))))
(COND ((CDR Z1) (RPLACD T2 (CDR Z1)) (SETQ T2 (LAST T2))))
B (SETQ L (CDR L))
(GO A)))
EXPR)
(DEFPROP TIMEIT
(LAMBDA NIL (DIFFERENCE (DIFFERENCE (TIME) (GCTIME)) TIME1))
EXPR)
(DEFPROP TREE
(LAMBDA(L)
(COND ((ATOM (CDR (ANCESTOR L))) (LIST L))
(T (NCONC (LIST L) (TREE (CAR (ANCESTOR L))) (TREE (CDR (ANCESTOR L)))))))
EXPR)
(DEFPROP TREEDEP
(LAMBDA(X)
(PROG (Z)
(SETQ Z (ANCESTOR X))
(COND ((ATOM (CDR Z)) (RETURN 0)) (T (RETURN (ADD1 (MAX (TREEDEP (CAR Z)) (TREEDEP (CDR Z)))))))))
EXPR)
(DEFPROP TRY
(LAMBDA (L) (PROG (AUTO) (EVAL (CONS (QUOTE TRY1) L))))
FEXPR)
(DEFPROP TRY1
(LAMBDA(L)
(PROG (FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
(SETQ PRNO 0)
T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
(SETQ Z (CAR (LAST L)))
(SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
(EVAL (CONS (QUOTE INPUT) L))
(INC T)
P3 B (SETQ Z2 (INCLAUSES))
(INC NIL)
(COND ((NULL Z2) (RETURN NIL)))
(SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
(SETQ Z2 (ATTEMPT Z2 NIL NIL))
A (COND ((NULL Z2) (RETURN (QUOTE *)))
((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
((EQ (CAR Z2) (QUOTE ABORT))
(SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
(GO A)))
FEXPR)
(DEFPROP TRYPRF
(LAMBDA(U)
(PROG (Z1 Z2 R)
TRY4 TRY3
(SETQ XX (CHOICE XX EE EE1))
(COND ((NULL XX) (GO TRY7)) ((EQ XX T) (GO TRY7)))
(SETQ Z1 (CAAR XX))
(SETQ Z2 (CADR XX))
(COND ((OR (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6F)))
TRY2 TRY1
(COND ((NOT STRATEGY) (GO TRY1A)))
(COND ((STRATEGY Z1 Z2) (GO TRY1A)) (T (GO TRY6F)))
TRY1A
(COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)) ((AND (ALLNEG Z1) (ALLNEG Z2)) (GO TRY8)))
(SETQ R (RESOLVE Z1 Z2))
TRY10
(COND ((NULL R) (GO TRY6A)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
(SETQ CNT (PLUS CNT (FINI U R Z1 Z2 EE1)))
TRY6A
TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6F)))
(SETQ R (PARMOD Z1 Z2))
(COND ((NULL R) (GO TRY6F)))
(SETQ CNT (PLUS CNT (FINI U R Z1 Z2 EE1)))
TRY6F
TRY6G
TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
(GO TRY3)
TRY7 (PRINT (QUOTE COUNT))
(PRINT COUNT)
(PRINT (QUOTE LEVEL))
(PRINT LVL)
(SETQ LVL (ADD1 LVL))
(PRINT (QUOTE ELAPSED-TIME))
(PRINT (TIMEIT))
(SETQ EE EE1)
(SETQ XX (CONS U EE))
(COND ((CDR EE) (SETQ EE1 (LAST EE)) (GO TRY4)))
(PRINT (QUOTE NO-PROOF-FOUND))
(COND (AUTO (ERR (QUOTE NOPROOF))))
(UPDATE CLAUSES)
(ERR (QUOTE NOPROOF))
TRY6H))
EXPR)
(DEFPROP TRAVERSE
(LAMBDA(L)
(PROG (Z Z1 Z2)
(SETQ Z (ANCESTOR L))
(SETQ Z1 (CAR Z))
(SETQ Z (CDR Z))
(COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
(COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
(RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
EXPR)
(DEFPROP UNIT
(LAMBDA (X) (EQ (NUM X) 1))
EXPR)
(DEFPROP UNITS
(LAMBDA(U)
(PROG (Z Z1)
(COND ((NULL U) (RETURN NIL)))
(SETQ Z U)
UN1 (COND ((EQ (NUM (CAR Z)) 1) (SETQ Z1 (CONS (CAR Z) Z1))))
(SETQ Z (CDR Z))
(COND (Z (GO UN1)))
(RETURN Z1)))
EXPR)
(DEFPROP UNITRES
(LAMBDA(C UP UN)
(PROG (C1 Z1 U Z RES)
(SETQ C1 C)
(COND ((AND (ALLPOS C) (NULL UN)) (RETURN NIL)) ((AND (ALLNEG C) (NULL UP)) (RETURN NIL)))
(COND ((NULL UN) (SETQ C (NEGL C)) (GO N)))
(SETQ C (CDR C))
B (SETQ Z1 (CAR C))
(COND ((NEG Z1) (GO N)))
(SETQ U UN)
A (COND ((NOT (EQ (CAR Z1) (CADAR (CAR U)))) (GO A1)))
(SETQ Z (UNI (CDDADR (CAR U)) (CDR Z1) NIL))
(COND ((NULL Z) (GO A1)))
(COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
(SETQ RES (CONS (REDUCER C1 C) RES))
(GO A2)
A1 (SETQ U (CDR U))
(COND (U (GO A)))
A2 (SETQ C (CDR C))
(COND (C (GO B)) (T (RETURN RES)))
N (SETQ Z1 (CDAR C))
(SETQ U UP)
C (COND ((NULL U) (RETURN RES)))
C2 (COND ((NOT (EQ (CAR Z1) (CAADAR U))) (GO C1)))
(SETQ Z (UNI (CDADAR U) (CDR Z1) NIL))
(COND ((NULL Z) (GO C1)) ((UNIT C1) (RETURN (LIST NIL))))
(SETQ RES (CONS (REDUCER C1 C) RES))
(GO C3)
C1 (SETQ U (CDR U))
(COND (U (GO C2)))
C3 (SETQ C (CDR C))
(COND (C (GO N)) (T (RETURN RES)))))
EXPR)
(DEFPROP UNITREDUCT
(LAMBDA(R UP UN)
(PROG (Z UP1 UN1 C1 C2 RC1 RC2)
(SETQ UN1 (SETQ UP1 NIL))
(SETQ C1 (SETQ C2 R))
A (SETQ RC1 (SETQ RC2 NIL))
(COND ((NULL C2) (GO C1)) ((AND (NULL UP1) (NULL UN1)) (GO C)))
B (SETQ Z (UNITRES (CAR C2) UP1 UN1))
(COND ((NULL Z) (SETQ RC2 (CONS (CAR C2) RC2)))
((NULL (CAR Z)) (RETURN (LIST NIL)))
(T (SETQ RC1 (APPEND Z RC1))))
(SETQ C2 (CDR C2))
(COND (C2 (GO B)))
C1 (SETQ UP (APPEND UP1 UP))
(SETQ UN (APPEND UN1 UN))
C (SETQ Z (UNITRES (CAR C1) UP UN))
(COND ((NULL Z) (SETQ RC2 (CONS (CAR C1) RC2)))
((NULL (CAR Z)) (RETURN (LIST NIL)))
(T (SETQ RC1 (APPEND Z RC1))))
(SETQ C1 (CDR C1))
(COND (C1 (GO C)))
(COND ((NULL RC1) (RETURN RC2)))
(SETQ C2 RC2)
(SETQ C1 RC1)
(SETQ Z (UNITPN C1))
(COND ((AND (NULL (CAR Z)) (NULL (CDR Z))) (RETURN (APPEND RC1 RC2))))
(SETQ UP1 (CAR Z))
(SETQ UN1 (CDR Z))
(GO A)))
EXPR)
(DEFPROP UNITPN
(LAMBDA(X)
(PROG (P N)
A (COND
((UNIT (CAR X)) (COND ((ALLPOS (CAR X)) (SETQ P (CONS (CAR X) P))) (T (SETQ N (CONS (CAR X) N))))))
(SETQ X (CDR X))
(COND (X (GO A)))
(RETURN (CONS P N))))
EXPR)
(DEFPROP UNIFY
(LAMBDA(X Y)
(PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
(SETQ LC (LIST NIL))
U3 (SETQ Z1 (CAR X))
(SETQ Z2 (CAR Y))
(COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
(COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
(COND ((VAR Z3)
(COND ((VAR Z4) (GO UN1))
((CONST Z4) (GO UN3))
(T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
(COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
((VAR Z4)
(COND ((CONST Z3) (GO UN1))
(T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z4 (COPY Z3)))) (GO UN2))
((NOT (VAR Z1)) (SETQ Z3 (SUBS3T* (CDR LC) Z3))))
(COND ((OCCUR Z4 (CDR Z3)) (RETURN NIL)) (T (GO UN1))))))
((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
(SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
(SETQ X (APPEND Z6 (CDR X)))
(SETQ Y (APPEND Z7 (CDR Y)))
(GO U3))
(T (RETURN NIL)))
UN1 (SUBS2T Z3 Z4 LC)
UN2 (SETQ X (CDR X))
(COND (X (SETQ Y (CDR Y)) (GO U3)))
(RETURN LC)
UN3 (SUBS2T Z4 Z3 LC)
(GO UN2)))
EXPR)
(DEFPROP UNI
(LAMBDA(C D L)
(PROG (Z1 Z2 Z3)
UN2 (SETQ Z2 (CAR D))
(SETQ Z1 (SETQ Z3 (CAR C)))
(COND
((VAR Z1) (SETQ Z3 (SEARCH1 Z1 L))
(COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
(COND ((VAR Z2) (RETURN NIL))
((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
((VAR Z1) (COND ((EQUAL Z2 Z3) (GO UN1)) (T (RETURN NIL))))
((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
(SETQ D (APPEND (CDR Z2) (CDR D)))
(GO UN2))
(T (RETURN NIL)))
UN1 (SETQ C (CDR C))
(COND (C (SETQ D (CDR D)) (GO UN2)))
(COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64)))))))
EXPR)
(DEFPROP UNION
(LAMBDA(Z C D YC YD)
(PROG (BL L Z1 Z2 Z3 Z4 Z5 Z6 C1 C2 NEG RES M1 Z7 Z8)
(SETQ NO* NO)
(COND
(ORDER (COND (ANCESTRY (SETQ SAT C) (SETQ L YC)) ((EQ C SAT) (SETQ L YC)) (T (SETQ L YD)))
(COND ((< L (CDR SAT)) (RETURN NIL)))))
(SETQ M1 0)
(SETQ Z7 (ANCESTOR C))
(SETQ Z8 (ANCESTOR D))
(SETQ C (CDR C))
(SETQ D (CDR D))
(SETQ Z1 Z)
(SETQ Z2 Z)
(SETQ Z3 (SUBS3T** Z1 YC))
(SETQ Z4 (SUBS3T** Z2 YD))
UN1 (SETQ Z5 (SUBS3T** Z1 (CAR C)))
(COND ((OR (EQUAL Z3 Z5) (MEMC Z5 C1)) (SETQ M1 (ADD1 M1)) (GO UN1A))
((AND (NEG Z5) (MEMC (CDR Z5) C1)) (RETURN NIL)))
(SETQ C1 (CONS Z5 C1))
UN1A (SETQ C (CDR C))
(COND (C (GO UN1)))
UN2 (SETQ Z6 (SUBS3T** Z2 (CAR D)))
(COND ((AND PARRES (EQUAL Z4 Z6)) (SETQ Z6 PARRES) (GO UN2B))
((OR (EQUAL Z4 Z6) (MEMC Z6 C2)) (SETQ M1 (ADD1 M1)) (GO UN2A))
((NEG Z6) (COND ((OR (MEMC (CDR Z6) C1) (MEMC (CDR Z6) C2)) (RETURN NIL))))
((POS Z6) (COND ((MEMBER (CONS ESCAPE Z6) C1) (RETURN NIL)))))
UN2B (SETQ C2 (CONS Z6 C2))
UN2A (SETQ D (CDR D))
(COND (D (GO UN2)))
(SETQ Z2 0)
(COND ((NULL C1) (COND ((NULL C2) (RETURN (LIST NIL))) (T (SETQ Z1 C2) (GO UN7))))
((NULL C2) (SETQ Z1 C1) (GO UN7)))
(COND ((AND MERGE (EQ M1 2) (CDR Z7) (CDR Z8)) (RETURN NIL)))
UN5 (SETQ NEG RES)
(COND ((NULL C1) (SETQ Z1 C2) (GO UN7))
((NULL C2) (SETQ Z1 C1) (GO UN7))
((AND (POS (CAR C1)) (POS (CAR C2))) (GO UN3))
((AND (POS (CAR C1)) (NEG (CAR C2))) (GO UN6))
((OR (AND (NEG (CAR C1)) (POS (CAR C2))) (NOT (ORDERP (CADAR C1) (CADAR C2))))
(SETQ Z1 (CAR C1))
(SETQ C1 (CDR C1))
(GO UN4)))
UN6 (SETQ Z1 (CAR C2))
(SETQ C2 (CDR C2))
UN4 (UPIT Z1)
(COND ((MEMBER Z1 RES) (GO UN5)) (T (SETQ Z2 (ADD1 Z2)) (SETQ RES (CONS Z1 RES)) (GO UN5)))
UN7 (COND ((NULL Z1) (RETURN (LIST (CONS (LIST Z2 NEG) RES)))) ((MEMBER (CAR Z1) RES) (GO UN8)))
(SETQ Z2 (ADD1 Z2))
(UPIT (CAR Z1))
(SETQ RES (CONS (CAR Z1) RES))
(COND ((NEG (CAR Z1)) (SETQ NEG RES)))
UN8 (SETQ Z1 (CDR Z1))
(GO UN7)
UN3 (COND ((NOT (ORDERP (CAAR C1) (CAAR C2))) (SETQ Z1 (CAR C1)) (SETQ C1 (CDR C1)) (GO UN4A)))
(SETQ Z1 (CAR C2))
(SETQ C2 (CDR C2))
UN4A (UPIT1 (CDR Z1))
(COND ((MEMBER Z1 RES) (GO UN5A)))
(SETQ Z2 (ADD1 Z2))
(SETQ RES (CONS Z1 RES))
UN5A (COND ((NULL C1) (SETQ Z1 C2) (GO UN7)) ((NULL C2) (SETQ Z1 C1) (GO UN7)))
(GO UN3)))
EXPR)
(DEFPROP UNWIND
(LAMBDA(X1 X2 Y Z N)
(PROG (Z1 Z2)
(SETQ Z2 (ASSOC1 X1 Z))
(COND (Z2 (SETQ Z1 (CDR Z2)) (GO A)))
(NCONC Y (COPYDELETED X1))
(NCONC Z (LIST (CONS (LAST Y) N)))
(SETQ Z1 N)
(SETQ N (ADD1 N))
A (SETQ Z2 (ASSOC1 X2 Z))
(COND (Z2 (RETURN (CONS (CONS Z1 (CDR Z2)) N))))
(NCONC Y (COPYDELETED X2))
(NCONC Z (LIST (CONS (LAST Y) N)))
(RETURN (CONS (CONS Z1 N) (ADD1 N)))))
EXPR)
(DEFPROP UPDATE
(LAMBDA(E)
(PROG (USINGFL USING
CHAN1
ELOC
CHAN
AUTO
DL1
RF
XYZ
XYZ1
CMD
LOCFLG
Z
Z1
Z2
INCT
Z3
UEX
Z1R
Z2R
N1
R
N
NAME
NAMELIST
ZZ)
(SETQ CHAN (OUTC NIL NIL))
(SETQ AXNO (QUOTE INSERT))
(SETQ FNNAM (QUOTE EDI))
(SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
(SETQ N1 (LAST NAMELIST))
(SETQ INCT (INC NIL))
U9 (SETQ ELOC E)
(SETQ N 1)
U3 (UP1A (CAR ELOC) N)
U3A (TERPRI)
U3AA (SETQ CMD (READ))
(COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
U3B (COND ((NOT (ATOM CMD)) (GO UPDATE1)))
U3C (SETQ CMD (EXPLODE CMD))
(COND ((EQ (LENGTH CMD) 1) (GO UER1))
((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
(GO U3A)
UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
(GO U3A)
UDI1 (SETQ Z1 (UPGETL E NAMELIST))
(COND ((NULL Z1) (GO U3A)))
(CLAUSES Z1)
(GO U3A)
USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
(SETQ Z NAMELIST)
USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
(SETQ Z (CDR Z))
(COND (Z (GO USY2)))
(GO U3A)
UFL2 (SETQ Z (QUOTE U))
(GO UFL4)
UFL3 (SETQ Z (QUOTE D))
(GO UFL4)
UFL1 (SETQ Z (CAR (EXPLODE (READ))))
UFL4 (SETQ Z2 405104)
(COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
(COND ((OR (NULL Z) (EQ (CAR Z )(QUOTE ABORT))) (GO U3A)))
(UPDATESTATE (CDDR Z))
(GO U3A)
UDE1 (SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (GO U3A)))
(EXPUNGE Z2)
(GO U3A)
UIN1 (SETQ NAME (READ))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (GO U3A)))
(COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
(NCONC Z1 Z2)
(GO U3A)
USU1 (SETQ Z1 (ERRSET (GETTERMS)))
(COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
((NULL (CAR Z1)) (GO U3A)))
(SETQ Z3 NIL)
(SETQ Z1 (CAR Z1))
USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (GO U12B)))
UUP1 (SETQ Z2 (UPGETNU))
(COND ((NUMBERP Z2) (GO U8)) (T (GO U3A)))
UDO1 (SETQ Z2 (UPGETNU))
(COND ((NUMBERP Z2) (GO U7)) (T (GO U3A)))
UAN1 (SETQ Z2 (UPGETL E NAMELIST))
UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
(SETQ Z2 (CDR Z2))
(GO UAN2)
UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
(INC INCT)
(OUTC CHAN NIL)
(SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
(SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
(RETURN (MINIMIZE (APPEND Z1 Z)))
USA1 (SETQ Z2 (UPGETL E NAMELIST))
(COND (Z2 (NCONC E Z2)))
(GO U3A)
UPA1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
(COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
(COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
(SETQ Z3 Z1)
USI2 (DEMOD (LIST (CAR Z3)) Z2)
(SETQ Z3 (CDR Z3))
(COND (Z3 (GO USI2)))
(PRINT (QUOTE CLAUSES-ARE:))
(CLAUSES Z1)
(GO U3A)
UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
(GO UUS3)
UCU1 (QUERY)
(GO U3A)
UDS1 (SETQ Z1 (READ))
(COND ((NOT (ATOM Z1)) (GO UDS3)))
UDS2 (COND
((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
(GO UDS2)))
UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
(GO U3A)
UEO1 (OUTC CHAN1 T)
(GO U3A)
UUS1 (SETQ NAME (QUOTE %USING))
(SETQ USINGFL T)
(SETQ USING NIL)
UUS3 (SETQ LOCFLG T)
UUS2 (SETQ Z2 (UPGETL E NAMELIST))
(SETQ USINGFL NIL)
(COND ((NULL Z2) (GO U3A)))
USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
(COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
(T (RPLACA (CAR N1) NAME)
(RPLACD (CAR N1) Z2)
(RPLACD N1 (CONS (CONS NIL NIL) NIL))
(SETQ N1 (CDR N1))))
(GO U3A)
USE1 (SETQ NAME (READ))
(SETQ LOCFLG NIL)
(GO UUS2)
UCL1 (SETQ Z (READ))
UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
(GO UCL2))
(T (GO U3A)))
UGO1 (SETQ Z1 (UPGETNU))
(COND ((NOT (NUMBERP Z1)) (GO U3A)))
(COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
(T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
UTR1 (SETQ UEX NIL)
(GO UEX2)
UEX1 (SETQ UEX T)
UEX2 (SETQ NAME (QUOTE LEMMA))
(SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
(COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
(SETQ AUTO T)
(SETQ Z2
(ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
(COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
(T NIL))
NIL))
(SETQ AUTO NIL)
(GO AT1A)
UST1 (STOP)
(GO U3A)
UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
(ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
U8 (COND ((EQ Z2 0) (GO U9)))
U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
(SETQ Z2 (DIFFERENCE Z2 5))
(SETQ ZZ 5)
U84 (SETQ Z N)
(SETQ Z3 (DIFFERENCE N ZZ))
(COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
(SETQ N Z3)
(SETQ Z3 ELOC)
(SETQ ELOC (DOWN N E))
(SETQ ZZ NIL)
(SETQ Z1 ELOC)
U81 (COND ((EQ Z1 Z3) (GO U82)))
(SETQ ZZ (CONS (CAR Z1) ZZ))
(SETQ Z1 (CDR Z1))
(GO U81)
U82 (COND ((NULL ZZ) (GO U83)))
(UP1A (CAR ZZ) (SUB1 Z))
(SETQ ZZ (CDR ZZ))
(SETQ Z (SUB1 Z))
(GO U82)
U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
(SETQ Z2 (PLUS Z2 N))
U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
(SETQ ELOC (CDR ELOC))
(SETQ N (ADD1 N))
(UP1A (CAR ELOC) N)
(COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
UPR1 (TERPRI)
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
(COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
(SETQ AXNO (QUOTE THEOREM))
(SETQ Z3 (NEGATE (CAR Z2)))
(SETQ AXNO (QUOTE INSERT))
(SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
(COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
(SETQ NAME (QUOTE LEMMA))
(SETQ LOCFLG T)
(GO USE2)
UME1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
(BAKSUB Z1 Z2)
(GO U3A)
UHE1 (PRINT MESSAGE)
(GO U3A)
URE1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
U%RE1
(SETQ RF T)
URE1A
(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
(SETQ Z1R Z1)
(SETQ Z2R Z2)
(SETQ Z3 NIL)
(COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
(COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
(COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
(COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
(SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
UR3A (SETQ Z2R (CDR Z2R))
(COND (Z2R (GO UR3)))
(SETQ Z1R (CDR Z1R))
(COND (Z1R (SETQ Z2R Z2) (GO UR3)))
UR3B (COND ((NULL Z3)
(COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
(T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
(RF (SETQ NAME (QUOTE RES)))
(T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
(SETQ Z2 Z3)
(SETQ LOCFLG T)
(GO AT2A)
UEV1 (PRINT (QUOTE EVAL-AWAITS))
(SETQ Z2 (ERRSET (EVAL (READ)) T))
(COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
(GO UEV1)
UPDATE1
(SETQ Z (EXPLODE (CAR CMD)))
(COND ((SETQ Z (ASSOC (READLIST (LIST (CAR Z) (CADR Z))) GOLIST1)) (GO (CDR Z))) (T (GO UER1)))
AT1 (COND ((NULL (SETQ Z1 (GETNAME (CADR CMD) NAMELIST))) (GO U3A)))
(SETQ NAME (CADR CMD))
(SETQ XYZ Z1)
(RPLACA (CDR CMD) (QUOTE XYZ))
(RPLACA CMD (QUOTE ATTEMPTUNTIL))
(SETQ Z2 (EVAL CMD))
AT1A (UPDATESTATE STRAT)
(COND
((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
(PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
(PRINC NAME)
(GO U3A))
((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
(SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
(SETQ AUTO NIL)
(GO AT1A))
((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
(SETQ Z2 (CADR Z2))
AT2A (SETQ N 1)
AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
(SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
(PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
(PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
(PRIN1 NAME)
(CLAUSES Z2)
(GO USE2)
S1 (COND ((NULL (SETQ XYZ (GETNAME (CADDDR CMD) NAMELIST))) (GO U3A)))
(RPLACA (CDDDR CMD) (QUOTE XYZ))
(RPLACA CMD (QUOTE SAVE))
(EVAL CMD)
(GO U3A)))
EXPR)
(DEFPROP UPGETL
(LAMBDA(E N)
(PROG (C N1 Z Z1 Z2 Z3 ZZ N2)
(SCANSET)
(START)
(SETQ C (ERRSET (<CLAUSES>) T))
(SCANRESET)
(COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
(SETQ C (TOP))
(COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
AS1 (SETQ Z (CAR C))
(COND ((ATOM Z)
(COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
(COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
(T (RETURN NIL))))
((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
(T (RETURN NIL))))
((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
(T (RETURN NIL)))
AS6 (SETQ C (CDR C))
(COND (C (GO AS1)) (T (RETURN ZZ)))
AS2 (SETQ Z2 (CADR Z))
(SETQ N1 (CAR Z))
(SETQ Z (CDR Z))
(SETQ Z3 Z1)
AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
AS3 (SETQ Z2 (SUB1 Z2))
(COND ((ZEROP Z2) (GO AS4)))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
AS4 (COND
((NOT (HERE (CAR Z1))) (PRINT N1)
(PRINC (QUOTE / ))
(PRINC (CAR Z))
(PRINC (QUOTE / ))
(PRINC (QUOTE HAS-BEEN-DELETED))
(RETURN NIL)))
(SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
(SETQ Z (CDR Z))
(COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
(GO AS6)
AS10 (SETQ N2 (QUOTE INSERT))
(SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF (FIXQFF (CDR Z)))))))
(GO AS6)
AS20 (SETQ N2 (QUOTE MATCHES))
(SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
(COND ((NULL Z) (GO AS6)) (T (GO AS31)))
AS30 (SETQ N2 (QUOTE INPUT))
(SETQ ZIN (CDR Z))
(COND
((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
(INC T)
(SETQ Z (INCLAUSES))
(INC NIL)
(COND ((NULL Z) (RETURN NIL)))
AS31 (SETQ ZZ (APPENDIT ZZ Z))
(GO AS6)))
EXPR)
(DEFPROP UPGETNU
(LAMBDA NIL
(PROG (Z)
(SETQ Z (READ))
A (COND ((NUMBERP Z) (RETURN Z)))
(SETQ Z (REVERSE (EXPLODE Z)))
(COND ((EQ (CAR Z) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z)))) (GO A)) (T (RETURN NIL)))))
EXPR)
(DEFPROP UPDATESTATE
(LAMBDA(L)
(PROG (L1)
(SETQ L1 STATEVECTOR)
A (COND ((NULL L) (RETURN NIL)))
(SET (CAR L1) (CAR L))
(SETQ L (CDR L))
(SETQ L1 (CDR L1))
(GO A)))
EXPR)
(DEFPROP UPIT
(LAMBDA (C) (COND ((NEG C) (UPIT1 (CDDR C))) (T (UPIT1 (CDR C)))))
EXPR)
(DEFPROP UPIT1
(LAMBDA(Z)
(PROG (Z1 Z2)
MAX2 (SETQ Z2 (CAR Z))
(COND ((VAR Z2) (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
((GREATERP Z2 NO*) NIL)
(T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO)))
(GO MAX1))
((CONST Z2) (GO MAX1))
(T (UPIT1 (CDR Z2))))
MAX1 (SETQ Z (CDR Z))
(COND (Z (GO MAX2)))
(RETURN NO)))
EXPR)
(DEFPROP UP1A
(LAMBDA(X N)
(PROG NIL
(TERPRI)
(PRINC N)
(PRINC (QUOTE / ))
(COND ((HERE X) (PRFPRINT (CDR X))) (T (PRINC (QUOTE *DE*))))
(RETURN NIL)))
EXPR)
(DEFPROP UP1B
(LAMBDA (X N) (PROG NIL (TERPRI) (PRINC N) (PRINC (QUOTE / )) (PRFPRINT (CDR X))))
EXPR)
(DEFPROP VARIT
(LAMBDA(Z)
(PROG (Z1 Z2 BL Z3)
(SETQ Z3 Z)
M1 (SETQ Z2 (CAR Z))
(COND ((VAR Z2)
(COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
(T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO))))
((EQ (CAR Z2) (QUOTE _)) (RPLACA Z (SETQ NO (ADD1 NO))))
((CONST Z2) NIL)
(T (VARIT (CDR Z2))))
(SETQ Z (CDR Z))
(COND (Z (GO M1)))
(RETURN Z3)))
EXPR)
(DEFPROP VINE
(LAMBDA (X) (NUMBERP (CDR (ANCESTOR X))))
EXPR)
(DEFPROP <
(LAMBDA(L X)
(PROG (Z Z1 Z2)
(SETQ Z X)
(COND ((NEG L) (SETQ L (CADR L)) (SETQ Z2 T)) (T (SETQ L (CAR L))))
A1 (SETQ Z1 (CAR Z))
(COND ((NEG Z1) (SETQ Z1 (CADR Z1))) (T (SETQ Z1 (CAR Z1))))
(COND ((NOT (ORDERP L Z1)) (GO A2))
((OR (AND (NOT Z2) (MEMBER Z1 PMODEL)) (AND Z2 (MEMBER Z1 NMODEL))) (RETURN T)))
A2 (SETQ Z (CDR Z))
(COND (Z (GO A1)))
(RETURN NIL)))
EXPR)